αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic

We present alpha leanTAP, a declarative tableau-based theorem prover written as a pure relation. Like leanTAP, on which it is based, alpha leanTAP can prove ground theorems in first-order classical logic. Since it is declarative, alpha 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 alpha leanTAP, beginning with a translation of leanTAP into alpha 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.