Skip to content
/ leanTAP Public

A Declarative Theorem Prover for First-Order Classical Logic

Notifications You must be signed in to change notification settings

namin/leanTAP

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

21 Commits
 
 
 
 
 
 

Repository files navigation

leanTAP: A Theorem Prover for First-Order Classical Logic

This project implements leanTAP in clojure.core.logic.nominal closely following the alphaleanTAP implementation described in alphaleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (PDF) and chapter of 10 of William E. Byrd's thesis (PDF).

The alphaleantap directory contains the original implementation in Scheme.

The cljtap directory contains the implementation in Clojure, using core.logic.nominal.

Statistics

On the Pelletier problems, the Clojure implementation is roughly 1/3 faster on average than the original implementation tested with Petite Chez Scheme.

Chart with Clojure and Scheme results on Pelletier Problems

Warning: the results in the spreadsheet are based on a single run of each implementation. It would still be interesting for core.logic's sake to understand why the implementation in Clojure performs much worse on Problem 20 than the original one in Petite Chez Scheme.

About

A Declarative Theorem Prover for First-Order Classical Logic

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published