Website  doi  abstract   bibtex   

@article{
 title = {α lean TA P: A declarative theorem prover for first-order classical logic},
 type = {article},
 year = {2008},
 keywords = {Classical logic; First order; Nominal logic; Prov,Computer programming; Logic programming; Programmi,Program translators; Theorem proving},
 pages = {238-252},
 volume = {5366 LNCS},
 websites = {https://www.scopus.com/inward/record.uri?eid=2-s2.0-58549102767&doi=10.1007%2F978-3-540-89982-2_26&partnerID=40&md5=f016be2ae9aa5d5b9df874840bae73ad},
 city = {Udine},
 id = {caa2cb36-cc91-3bfc-9f4f-906787be7c8a},
 created = {2018-01-08T19:03:42.174Z},
 file_attached = {false},
 profile_id = {42d295c0-0737-38d6-8b43-508cab6ea85d},
 last_modified = {2018-03-12T19:03:16.419Z},
 read = {false},
 starred = {false},
 authored = {true},
 confirmed = {true},
 hidden = {false},
 citation_key = {Near2008238},
 source_type = {article},
 notes = {cited By 1; Conference of 24th International Conference on Logic Programming, ICLP 2008 ; Conference Date: 9 December 2008 Through 13 December 2008; Conference Code:75119},
 folder_uuids = {a0f5ac31-a393-4a7b-b7db-64a126a80f6e},
 private_publication = {false},
 abstract = {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.},
 bibtype = {article},
 author = {Near, J P and Byrd, W E and Friedman, D P},
 doi = {10.1007/978-3-540-89982-2_26},
 journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}
}