Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.
YouTube Encyclopedic

1/5Views:77 9836 9298 7502 2221 204

Automated Mathematical Proofs  Computerphile

Automated Theorem Proving and Axiomatic Mathematics

What are the prospects for automatic theorem proving?

Josef Urban  AI and Theorem Proving

Motivation and State of the Art for the Lean Theorem Prover  Kevin Buzzard
Transcription
Logical foundations
While the roots of formalised logic go back to Aristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalised mathematics. Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially modern predicate logic.^{[1]} His Foundations of Arithmetic, published in 1884,^{[2]} expressed (parts of) mathematics in formal logic. This approach was continued by Russell and Whitehead in their influential Principia Mathematica, first published 1910–1913,^{[3]} and with a revised second edition in 1927.^{[4]} Russell and Whitehead thought they could derive all mathematical truth using axioms and inference rules of formal logic, in principle opening up the process to automatisation. In 1920, Thoralf Skolem simplified a previous result by Leopold Löwenheim, leading to the Löwenheim–Skolem theorem and, in 1930, to the notion of a Herbrand universe and a Herbrand interpretation that allowed (un)satisfiability of firstorder formulas (and hence the validity of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.^{[5]}
In 1929, Mojżesz Presburger showed that the theory of natural numbers with addition and equality (now called Presburger arithmetic in his honor) is decidable and gave an algorithm that could determine if a given sentence in the language was true or false.^{[6]}^{[7]} However, shortly after this positive result, Kurt Gödel published On Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), showing that in any sufficiently strong axiomatic system there are true statements which cannot be proved in the system. This topic was further developed in the 1930s by Alonzo Church and Alan Turing, who on the one hand gave two independent but equivalent definitions of computability, and on the other gave concrete examples for undecidable questions.
First implementations
Shortly after World War II, the first general purpose computers became available. In 1954, Martin Davis programmed Presburger's algorithm for a JOHNNIAC vacuum tube computer at the Institute for Advanced Study in Princeton, New Jersey. According to Davis, "Its great triumph was to prove that the sum of two even numbers is even".^{[7]}^{[8]} More ambitious was the Logic Theory Machine in 1956, a deduction system for the propositional logic of the Principia Mathematica, developed by Allen Newell, Herbert A. Simon and J. C. Shaw. Also running on a JOHNNIAC, the Logic Theory Machine constructed proofs from a small set of propositional axioms and three deduction rules: modus ponens, (propositional) variable substitution, and the replacement of formulas by their definition. The system used heuristic guidance, and managed to prove 38 of the first 52 theorems of the Principia.^{[7]}
The "heuristic" approach of the Logic Theory Machine tried to emulate human mathematicians, and could not guarantee that a proof could be found for every valid theorem even in principle. In contrast, other, more systematic algorithms achieved, at least theoretically, completeness for firstorder logic. Initial approaches relied on the results of Herbrand and Skolem to convert a firstorder formula into successively larger sets of propositional formulae by instantiating variables with terms from the Herbrand universe. The propositional formulas could then be checked for unsatisfiability using a number of methods. Gilmore's program used conversion to disjunctive normal form, a form in which the satisfiability of a formula is obvious.^{[7]}^{[9]}
Decidability of the problem
Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but coNPcomplete, and hence only exponentialtime algorithms are believed to exist for general proof tasks. For a first order predicate calculus, Gödel's completeness theorem states that the theorems (provable statements) are exactly the logically valid wellformed formulas, so identifying valid formulas is recursively enumerable: given unbounded resources, any valid formula can eventually be proven. However, invalid formulas (those that are not entailed by a given theory), cannot always be recognized.
The above applies to first order theories, such as Peano arithmetic. However, for a specific model that may be described by a first order theory, some statements may be true but undecidable in the theory used to describe the model. For example, by Gödel's incompleteness theorem, we know that any theory whose proper axioms are true for the natural numbers cannot prove all first order statements true for the natural numbers, even if the list of proper axioms is allowed to be infinite enumerable. It follows that an automated theorem prover will fail to terminate while searching for a proof precisely when the statement being investigated is undecidable in the theory being used, even if it is true in the model of interest. Despite this theoretical limit, in practice, theorem provers can solve many hard problems, even in models that are not fully described by any first order theory (such as the integers).
Related problems
A simpler, but related, problem is proof verification, where an existing proof for a theorem is certified valid. For this, it is generally required that each individual proof step can be verified by a primitive recursive function or program, and hence the problem is always decidable.
Since the proofs generated by automated theorem provers are typically very large, the problem of proof compression is crucial and various techniques aiming at making the prover's output smaller, and consequently more easily understandable and checkable, have been developed.
Proof assistants require a human user to give hints to the system. Depending on the degree of automation, the prover can essentially be reduced to a proof checker, with the user providing the proof in a formal way, or significant proof tasks can be performed automatically. Interactive provers are used for a variety of tasks, but even fully automatic systems have proved a number of interesting and hard theorems, including at least one that has eluded human mathematicians for a long time, namely the Robbins conjecture.^{[10]}^{[11]} However, these successes are sporadic, and work on hard problems usually requires a proficient user.
Another distinction is sometimes drawn between theorem proving and other techniques, where a process is considered to be theorem proving if it consists of a traditional proof, starting with axioms and producing new inference steps using rules of inference. Other techniques would include model checking, which, in the simplest case, involves bruteforce enumeration of many possible states (although the actual implementation of model checkers requires much cleverness, and does not simply reduce to brute force).
There are hybrid theorem proving systems which use model checking as an inference rule. There are also programs which were written to prove a particular theorem, with a (usually informal) proof that if the program finishes with a certain result, then the theorem is true. A good example of this was the machineaided proof of the four color theorem, which was very controversial as the first claimed mathematical proof which was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are called nonsurveyable proofs). Another example of a programassisted proof is the one that shows that the game of Connect Four can always be won by the first player.
Industrial uses
Commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. Since the Pentium FDIV bug, the complicated floating point units of modern microprocessors have been designed with extra scrutiny. AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
Firstorder theorem proving
In the late 1960s agencies funding research in automated deduction began to emphasize the need for practical applications. One of the first fruitful areas was that of program verification whereby firstorder theorem provers were applied to the problem of verifying the correctness of computer programs in languages such as Pascal, Ada, etc. Notable among early program verification systems was the Stanford Pascal Verifier developed by David Luckham at Stanford University.^{[12]}^{[13]}^{[14]} This was based on the Stanford Resolution Prover also developed at Stanford using John Alan Robinson's resolution principle. This was the first automated deduction system to demonstrate an ability to solve mathematical problems that were announced in the Notices of the American Mathematical Society before solutions were formally published.^{[citation needed]}
Firstorder theorem proving is one of the most mature subfields of automated theorem proving. The logic is expressive enough to allow the specification of arbitrary problems, often in a reasonably natural and intuitive way. On the other hand, it is still semidecidable, and a number of sound and complete calculi have been developed, enabling fully automated systems.^{[15]} More expressive logics, such as Higherorder logics, allow the convenient expression of a wider range of problems than first order logic, but theorem proving for these logics is less well developed.^{[16]}^{[17]}
Benchmarks, competitions, and sources
The quality of implemented systems has benefited from the existence of a large library of standard benchmark examples — the Thousands of Problems for Theorem Provers (TPTP) Problem Library^{[18]} — as well as from the CADE ATP System Competition (CASC), a yearly competition of firstorder systems for many important classes of firstorder problems.
Some important systems (all have won at least one CASC competition division) are listed below.
 E is a highperformance prover for full firstorder logic, but built on a purely equational calculus, originally developed in the automated reasoning group of Technical University of Munich under the direction of Wolfgang Bibel, and now at BadenWürttemberg Cooperative State University in Stuttgart.
 Otter, developed at the Argonne National Laboratory, is based on firstorder resolution and paramodulation. Otter has since been replaced by Prover9, which is paired with Mace4.
 SETHEO is a highperformance system based on the goaldirected model elimination calculus, originally developed by a team under direction of Wolfgang Bibel. E and SETHEO have been combined (with other systems) in the composite theorem prover ESETHEO.
 Vampire was originally developed and implemented at Manchester University by Andrei Voronkov and Krystof Hoder. It is now developed by a growing international team. It has won the FOF division (among other divisions) at the CADE ATP System Competition regularly since 2001.
 Waldmeister is a specialized system for unitequational firstorder logic developed by Arnim Buch and Thomas Hillenbrand. It won the CASC UEQ division for fourteen consecutive years (1997–2010).
 SPASS is a first order logic theorem prover with equality. This is developed by the research group Automation of Logic, Max Planck Institute for Computer Science.
The Theorem Prover Museum^{[19]} is an initiative to conserve the sources of theorem prover systems for future analysis, since they are important cultural/scientific artefacts. It has the sources of many of the systems mentioned above.
Popular techniques
 Firstorder resolution with unification
 Model elimination
 Method of analytic tableaux
 Superposition and term rewriting
 Model checking
 Mathematical induction^{[20]}
 Binary decision diagrams
 DPLL
 Higherorder unification
Software systems
Name  License type  Web service  Library  Standalone  Last update (YYYYmmdd format) 

ACL2  3clause BSD  No  No  Yes  May 2019 
Prover9/Otter  Public Domain  Via System on TPTP  Yes  No  2009 
Jape  GPLv2  Yes  Yes  No  May 15, 2015 
PVS  GPLv2  No  Yes  No  January 14, 2013 
EQP  ?  No  Yes  No  May 2009 
PhoX  ?  No  Yes  No  September 28, 2017 
E  GPL  Via System on TPTP  No  Yes  July 4, 2017 
SNARK  Mozilla Public License 1.1  No  Yes  No  2012 
Vampire  Vampire License  Via System on TPTP  Yes  Yes  December 14, 2017 
Theorem Proving System (TPS)  TPS Distribution Agreement  No  Yes  No  February 4, 2012 
SPASS  FreeBSD license  Yes  Yes  Yes  November 2005 
IsaPlanner  GPL  No  Yes  Yes  2007 
KeY  GPL  Yes  Yes  Yes  October 11, 2017 
Z3 Theorem Prover  MIT License  Yes  Yes  Yes  November 19, 2019 
Free software
 AltErgo
 Automath
 CVC
 E
 Gödel machine
 IsaPlanner
 LCF
 Mizar
 NuPRL
 Paradox
 Prover9
 PVS
 SPARK (programming language)
 Twelf
 Z3 Theorem Prover
Proprietary software
See also
 Curry–Howard correspondence
 Symbolic computation
 Ramanujan machine
 Computeraided proof
 Formal verification
 Logic programming
 Proof checking
 Model checking
 Proof complexity
 Computer algebra system
 Program analysis (computer science)
 General Problem Solver
 Metamath language for formalized mathematics
Notes
 ^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert.
 ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 20070926. Retrieved 20120902.
 ^ Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica (1st ed.). Cambridge University Press.
 ^ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press.
 ^ Herbrand, J. (1930). Recherches sur la théorie de la démonstration (PhD). University of Paris.
 ^ Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
 ^ ^{a} ^{b} ^{c} ^{d} Davis, Martin (2001). "The Early History of Automated Deduction". Robinson & Voronkov 2001.)
 ^ Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). Ki 2007. LNAI. Springer (4667): 2–18. Archived (PDF) from the original on 20221009. Retrieved 2 September 2012.
 ^ 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.
 ^ Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 20081011.
 ^ David C. Luckham and Norihisa Suzuki (Mar 1976). Automatic Program Verification V: VerificationOriented Proof Rules for Arrays, Records, and Pointers (Technical Report ADA027 455). Defense Technical Information Center. Archived from the original on August 12, 2021.
 ^ 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.
 ^ 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. CSTR79731.
 ^ 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: 224. doi:10.1145/12808.12833. ISBN 9780897912068. S2CID 14361631.
 ^ Kerber, Manfred. "How to prove higher order theorems in first order logic." (1999).
 ^ Benzmüller, Christoph, et al. "LEOIIa cooperative automatic theorem prover for classical higherorder logic (system description)." International Joint Conference on Automated Reasoning. Springer, Berlin, Heidelberg, 2008.
 ^ Sutcliffe, Geoff. "The TPTP Problem Library for Automated Theorem Proving". Retrieved 15 July 2019.
 ^ "The Theorem Prover Museum". Michael Kohlhase. Retrieved 20221120.
 ^ 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.
References
 Chang, ChinLiang; Lee, Richard CharTung (2014) [1973]. Symbolic Logic and Mechanical Theorem Proving. Elsevier. ISBN 9780080917283.
 Loveland, Donald W. (2016) [1978]. Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science. Vol. 6. Elsevier. ISBN 9781483296777.
 Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer. ISBN 9781461396871.
 Gallier, Jean H. (2015) [1986]. Logic for Computer Science: Foundations of Automatic Theorem Proving (2nd ed.). Dover. ISBN 9780486780825.
This material may be reproduced for any educational purpose, ...
 Duffy, David A. (1991). Principles of Automated Theorem Proving. Wiley. ISBN 9780471927846.
 Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim (1992). Automated Reasoning: Introduction and Applications (2nd ed.). McGraw–Hill. ISBN 9780079112514.
 Robinson, Alan; Voronkov, Andrei, eds. (2001). Handbook of Automated Reasoning. Vol. I. Elsevier, MIT Press. ISBN 9780080532790. II ISBN 9780262182232.
 Fitting, Melvin (2012) [1996]. FirstOrder Logic and Automated Theorem Proving (2nd ed.). Springer. ISBN 9781461223603.