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 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.
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.