α lean TA P: A declarative theorem prover for first-order classical logic. Near, J., P., Byrd, W., E., & Friedman, D., P. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5366 LNCS:238-252, 2008. ![α lean TA P: A declarative theorem prover for first-order classical logic [link]](https://bibbase.org/img/filetypes/link.svg "link")
Website doi abstract bibtex 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.
@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)}
}
Downloads: 0
{"_id":"bmSP9r8JWXAKzkhvu","bibbaseid":"near-byrd-friedman-leantapadeclarativetheoremproverforfirstorderclassicallogic-2008","downloads":0,"creationDate":"2018-03-12T19:10:28.069Z","title":"α lean TA P: A declarative theorem prover for first-order classical logic","author_short":["Near, J., P.","Byrd, W., E.","Friedman, D., P."],"year":2008,"bibtype":"article","biburl":"https://bibbase.org/service/mendeley/42d295c0-0737-38d6-8b43-508cab6ea85d","bibdata":{"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)","bibtex":"@article{\n title = {α lean TA P: A declarative theorem prover for first-order classical logic},\n type = {article},\n year = {2008},\n keywords = {Classical logic; First order; Nominal logic; Prov,Computer programming; Logic programming; Programmi,Program translators; Theorem proving},\n pages = {238-252},\n volume = {5366 LNCS},\n 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},\n city = {Udine},\n id = {caa2cb36-cc91-3bfc-9f4f-906787be7c8a},\n created = {2018-01-08T19:03:42.174Z},\n file_attached = {false},\n profile_id = {42d295c0-0737-38d6-8b43-508cab6ea85d},\n last_modified = {2018-03-12T19:03:16.419Z},\n read = {false},\n starred = {false},\n authored = {true},\n confirmed = {true},\n hidden = {false},\n citation_key = {Near2008238},\n source_type = {article},\n 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},\n folder_uuids = {a0f5ac31-a393-4a7b-b7db-64a126a80f6e},\n private_publication = {false},\n 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.},\n bibtype = {article},\n author = {Near, J P and Byrd, W E and Friedman, D P},\n doi = {10.1007/978-3-540-89982-2_26},\n journal = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}\n}","author_short":["Near, J., P.","Byrd, W., E.","Friedman, D., P."],"urls":{"Website":"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"},"biburl":"https://bibbase.org/service/mendeley/42d295c0-0737-38d6-8b43-508cab6ea85d","bibbaseid":"near-byrd-friedman-leantapadeclarativetheoremproverforfirstorderclassicallogic-2008","role":"author","keyword":["Classical logic; First order; Nominal logic; Prov","Computer programming; Logic programming; Programmi","Program translators; Theorem proving"],"metadata":{"authorlinks":{}},"downloads":0},"search_terms":["lean","declarative","theorem","prover","first","order","classical","logic","near","byrd","friedman"],"keywords":["classical logic; first order; nominal logic; prov","computer programming; logic programming; programmi","program translators; theorem proving"],"authorIDs":[],"dataSources":["zgahneP4uAjKbudrQ","ya2CyA73rpZseyrZ8","2252seNhipfTmjEBQ"]}