Automated theorem proving (English Wikipedia)

Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02.

aclanthology.org

Bos, Johan. "Wide-coverage semantic analysis with boxer." Semantics in text processing. step 2008 conference proceedings. 2008.

archive.org

Russell, Bertrand; Whitehead, Alfred North (1910–1913). Principia Mathematica (1st ed.). Cambridge University Press.
Russell, Bertrand; Whitehead, Alfred North (1927). Principia Mathematica (2nd ed.). Cambridge University Press.

bnf.fr

gallica.bnf.fr

Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert.

doi.org

Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation". IBM Journal of Research and Development. 4: 28–35. doi:10.1147/rd.41.0028.
McCune, W. W. (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881. S2CID 30847540.
Goel, Shilpi; Ray, Sandip (2022), Chattopadhyay, Anupam (ed.), "Microprocessor Assurance and the Role of Theorem Proving", Handbook of Computer Architecture, Singapore: Springer Nature Singapore, pp. 1–43, doi:10.1007/978-981-15-6401-7_38-1, ISBN 978-981-15-6401-7, retrieved 2024-02-10
Meng, Jia; Paulson, Lawrence C. (2008-01-01). "Translating Higher-Order Clauses to First-Order Clauses". Journal of Automated Reasoning. 40 (1): 35–60. doi:10.1007/s10817-007-9085-y. ISSN 1573-0670. S2CID 7716709.
Luckham, David C.; Suzuki, Norihisa (Oct 1979). "Verification of Array, Record, and Pointer Operations in Pascal". ACM Transactions on Programming Languages and Systems. 1 (2): 226–244. doi:10.1145/357073.357078. S2CID 10088183.
Loveland, D. W. (1986). "Automated theorem proving: Mapping logic into AI". Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems. Knoxville, Tennessee, United States: ACM Press. p. 224. doi:10.1145/12808.12833. ISBN 978-0-89791-206-8. S2CID 14361631.
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers". Journal of Automated Reasoning. 51 (1): 109–128. doi:10.1007/s10817-013-9278-5. ISSN 1573-0670. S2CID 5389933. ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.
Weber, Tjark; Conchon, Sylvain; Déharbe, David; Heizmann, Matthias; Niemetz, Aina; Reger, Giles (2019-01-01). "The SMT Competition 2015–2018". Journal on Satisfiability, Boolean Modeling and Computation. 11 (1): 221–259. doi:10.3233/SAT190123. In recent years, we have seen a blurring of lines between SMT-COMP and CASC with SMT solvers competing in CASC and ATPs competing in SMT-COMP.

dtic.mil

apps.dtic.mil

Luckham, David C.; Suzuki, Norihisa (Mar 1976). Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers (Technical Report AD-A027 455). Defense Technical Information Center. Archived from the original on August 12, 2021.

ed.ac.uk

era.lib.ed.ac.uk

Bundy, Alan (1999). The automation of proof by mathematical induction (PDF) (Technical report). Informatics Research Report. Vol. 2. Division of Informatics, University of Edinburgh. hdl:1842/3394.

eudml.org

Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD) (in French). University of Paris.

fu-berlin.de

page.mi.fu-berlin.de

Benzmüller, Christoph, et al. "LEO-II-a cooperative automatic theorem prover for classical higher-order logic (system description)." International Joint Conference on Automated Reasoning. Berlin, Germany and Heidelberg: Springer, 2008.

ghostarchive.org

Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). Ki 2007. LNAI (4667). Springer: 2–18. Archived (PDF) from the original on 2022-10-09. Retrieved 2 September 2012.

handle.net

hdl.handle.net

Bundy, Alan (1999). The automation of proof by mathematical induction (PDF) (Technical report). Informatics Research Report. Vol. 2. Division of Informatics, University of Edinburgh. hdl:1842/3394.

intellektik.de

Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). Ki 2007. LNAI (4667). Springer: 2–18. Archived (PDF) from the original on 2022-10-09. Retrieved 2 September 2012.

mpg.de

pure.mpg.de

Gabbay, Dov M., and Hans Jürgen Ohlbach. "Quantifier elimination in second-order predicate logic." (1992).

nytimes.com

Kolata, Gina (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 2008-10-11.

nyu.edu

cs.nyu.edu

Davis, Martin (2001). "The Early History of Automated Deduction". Robinson & Voronkov 2001. Archived from the original on 2012-07-28. Retrieved 2012-09-08. Robinson, Alan; Voronkov, Andrei, eds. (2001). Handbook of Automated Reasoning. Vol. I. Elsevier, MIT Press. ISBN 9780080532790. II ISBN 9780262182232.

philarchive.org

Muskens, Reinhard. "Combining Montague semantics and discourse representation." Linguistics and philosophy (1996): 143-186.

psu.edu

citeseerx.ist.psu.edu

Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). "Synthesis of programs in computational logic". In M. Bruynooghe and K.-K. Lau (ed.). Program Development in Computational Logic. LNCS. Vol. 3049. Springer. pp. 30–65. CiteSeerX 10.1.1.62.4976.

semanticscholar.org

api.semanticscholar.org

McCune, W. W. (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881. S2CID 30847540.
Meng, Jia; Paulson, Lawrence C. (2008-01-01). "Translating Higher-Order Clauses to First-Order Clauses". Journal of Automated Reasoning. 40 (1): 35–60. doi:10.1007/s10817-007-9085-y. ISSN 1573-0670. S2CID 7716709.
Luckham, David C.; Suzuki, Norihisa (Oct 1979). "Verification of Array, Record, and Pointer Operations in Pascal". ACM Transactions on Programming Languages and Systems. 1 (2): 226–244. doi:10.1145/357073.357078. S2CID 10088183.
Loveland, D. W. (1986). "Automated theorem proving: Mapping logic into AI". Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems. Knoxville, Tennessee, United States: ACM Press. p. 224. doi:10.1145/12808.12833. ISBN 978-0-89791-206-8. S2CID 14361631.
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers". Journal of Automated Reasoning. 51 (1): 109–128. doi:10.1007/s10817-013-9278-5. ISSN 1573-0670. S2CID 5389933. ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.

springer.com

link.springer.com

Goel, Shilpi; Ray, Sandip (2022), Chattopadhyay, Anupam (ed.), "Microprocessor Assurance and the Role of Theorem Proving", Handbook of Computer Architecture, Singapore: Springer Nature Singapore, pp. 1–43, doi:10.1007/978-981-15-6401-7_38-1, ISBN 978-981-15-6401-7, retrieved 2024-02-10

stanford.edu

exhibits.stanford.edu

Luckham, D.; German, S.; von Henke, F.; Karp, R.; Milne, P.; Oppen, D.; Polak, W.; Scherlis, W. (1979). Stanford Pascal verifier user manual (Technical report). Stanford University. CS-TR-79-731.

theoremprover-museum.github.io

"The Theorem Prover Museum". Michael Kohlhase. Retrieved 2022-11-20.

tptp.org

Sutcliffe, Geoff. "The TPTP Problem Library for Automated Theorem Proving". Retrieved 15 July 2019.

uni-kl.de

kluedo.ub.uni-kl.de

Kerber, Manfred. "How to prove higher order theorems in first order logic." (1999).

vprover.github.io

"History". vprover.github.io.

web.archive.org

Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02.
Davis, Martin (2001). "The Early History of Automated Deduction". Robinson & Voronkov 2001. Archived from the original on 2012-07-28. Retrieved 2012-09-08. Robinson, Alan; Voronkov, Andrei, eds. (2001). Handbook of Automated Reasoning. Vol. I. Elsevier, MIT Press. ISBN 9780080532790. II ISBN 9780262182232.
Luckham, David C.; Suzuki, Norihisa (Mar 1976). Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers (Technical Report AD-A027 455). Defense Technical Information Center. Archived from the original on August 12, 2021.

worldcat.org

Meng, Jia; Paulson, Lawrence C. (2008-01-01). "Translating Higher-Order Clauses to First-Order Clauses". Journal of Automated Reasoning. 40 (1): 35–60. doi:10.1007/s10817-007-9085-y. ISSN 1573-0670. S2CID 7716709.
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers". Journal of Automated Reasoning. 51 (1): 109–128. doi:10.1007/s10817-013-9278-5. ISSN 1573-0670. S2CID 5389933. ATPs and SMT solvers have complementary strengths. The former handle quantifiers more elegantly, whereas the latter excel on large, mostly ground problems.