α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 eanTAP, 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.