Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
verfasst von : Joseph P. Near, William E. Byrd, Daniel P. Friedman
Erschienen in: Logic Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.