α 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 = {49f0022f-259a-3b10-9588-694868fc6d9f},
created = {2018-03-13T18:36:23.956Z},
file_attached = {false},
profile_id = {42d295c0-0737-38d6-8b43-508cab6ea85d},
group_id = {be743863-c45b-320e-a8f8-6b8511f39f77},
last_modified = {2018-03-13T18:36:23.956Z},
read = {false},
starred = {false},
authored = {false},
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},
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":"49f0022f-259a-3b10-9588-694868fc6d9f","created":"2018-03-13T18:36:23.956Z","file_attached":false,"profile_id":"42d295c0-0737-38d6-8b43-508cab6ea85d","group_id":"be743863-c45b-320e-a8f8-6b8511f39f77","last_modified":"2018-03-13T18:36:23.956Z","read":false,"starred":false,"authored":false,"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","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 = {49f0022f-259a-3b10-9588-694868fc6d9f},\n created = {2018-03-13T18:36:23.956Z},\n file_attached = {false},\n profile_id = {42d295c0-0737-38d6-8b43-508cab6ea85d},\n group_id = {be743863-c45b-320e-a8f8-6b8511f39f77},\n last_modified = {2018-03-13T18:36:23.956Z},\n read = {false},\n starred = {false},\n authored = {false},\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 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"]}