αleanTAP: a declarative theorem prover for first-order classical logic. We present αleanTAP, a declarative tableau-based theorem prover written as a pure relation. Like leanTAP, on which it is based, αleanTAP can prove ground theorems in first-order classical logic. Since it is declarative, αleanTAP generates theorems and accepts non-ground theorems and proofs. The lack of mode restrictions also allows the user to provide guidance in proving complex theorems and to ask the prover to instantiate non-ground parts of theorems. We present a complete implementation of αleanTAP, beginning with a translation of leanTAP into αKanren, an embedding of nominal logic programming in Scheme. We then show how to use a combination of tagging and nominal unification to eliminate the impure operators inherited from leanTAP, resulting in a purely declarative theorem prover.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Near, Joseph P.; Byrd, William E.; Friedman, Daniel P.: $\alpha$\ssflean\itTAP: a declarative theorem prover for first-order classical logic (2008)