We present α lean TA P, a declarative tableau-based theorem prover written as a pure relation. Like lean TA P, on which it is based, α lean TA P can prove ground theorems in first-order classical logic. Since it is declarative, α lean TA P 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 α lean TA P, beginning with a translation of lean TA P 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 lean TA P, resulting in a purely declarative theorem prover. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Near, J. P., Byrd, W. E., & Friedman, D. P. (2008). α lean TA P: A declarative theorem prover for first-order classical logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5366 LNCS, pp. 238–252). https://doi.org/10.1007/978-3-540-89982-2_26
Mendeley helps you to discover research relevant for your work.