Automated theorem proving (also known asATP orautomated deduction) is a subfield ofautomated reasoning andmathematical logic dealing with provingmathematical theorems bycomputer programs. Automated reasoning overmathematical proof was a major motivating factor for the development ofcomputer science.

While the roots of formalizedlogic go back toAristotle, the end of the 19th and early 20th centuries saw the development of modern logic and formalized mathematics.Frege'sBegriffsschrift (1879) introduced both a completepropositional calculus and what is essentially modernpredicate logic.^[1] HisFoundations of Arithmetic, published in 1884,^[2] expressed (parts of) mathematics in formal logic. This approach was continued byRussell andWhitehead in their influentialPrincipia 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 usingaxioms andinference rules of formal logic, in principle opening up the process to automation. In 1920,Thoralf Skolem simplified a previous result byLeopold Löwenheim, leading to theLöwenheim–Skolem theorem and, in 1930, to the notion of aHerbrand universe and aHerbrand interpretation that allowed(un)satisfiability of first-order formulas (and hence thevalidity of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.^[5]

In 1929,Mojżesz Presburger showed that thefirst-order theory of thenatural numbers with addition and equality (now calledPresburger arithmetic in his honor) isdecidable and gave an algorithm that could determine if a givensentence in thelanguage was true or false.^[6][7]

However, shortly after this positive result,Kurt Gödel publishedOn Formally Undecidable Propositions of Principia Mathematica and Related Systems (1931), showing that in any sufficiently strong axiomatic system, there are true statements that cannot be proved in the system. This topic was further developed in the 1930s byAlonzo Church andAlan Turing, who on the one hand gave two independent but equivalent definitions ofcomputability, and on the other gave concrete examples ofundecidable questions.

In 1954,Martin Davis programmed Presburger's algorithm for aJOHNNIACvacuum-tube computer at theInstitute 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 theLogic Theorist in 1956, a deduction system for thepropositional logic of thePrincipia Mathematica, developed byAllen Newell,Herbert A. Simon andJ. C. Shaw. Also running on a JOHNNIAC, the Logic Theorist 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 usedheuristic guidance, and managed to prove 38 of the first 52 theorems of thePrincipia.^[7]

The "heuristic" approach of the Logic Theorist 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 first-order logic. Initial approaches relied on the results ofHerbrand andSkolem to convert a first-order formula into successively larger sets ofpropositional formulae by instantiating variables withterms from theHerbrand universe. The propositional formulas could then be checked for unsatisfiability using a number of methods. Gilmore's program used conversion todisjunctive normal form, a form in which the satisfiability of a formula is obvious.^[7][9]

This sectiondoes notcite anysources. Please helpimprove this section byadding citations to reliable sources. Unsourced material may be challenged andremoved.(April 2010) (Learn how and when to remove this message)

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the common case ofpropositional logic, the problem is decidable butco-NP-complete, and hence onlyexponential-time algorithms are believed to exist for general proof tasks. For afirst-order predicate calculus,Gödel's completeness theorem states that the theorems (provable statements) are exactly the semantically validwell-formed formulas, so the valid formulas arecomputably enumerable: given unbounded resources, any valid formula can eventually be proven. However,invalid formulas (those that arenot entailed by a given theory), cannot always be recognized.

The above applies to first-order theories, such asPeano 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, byGödel's incompleteness theorem, we know that any consistent theory whose axioms are true for the natural numbers cannot prove all first-order statements true for the natural numbers, even if the list of 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 theintegers).

A simpler, but related, problem isproof 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 aprimitive 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 ofproof 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 theRobbins 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 includemodel checking, which, in the simplest case, involves brute-force 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 that use model checking as an inference rule. There are also programs that 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 machine-aided proof of thefour color theorem, which was very controversial as the first claimed mathematical proof that was essentially impossible to verify by humans due to the enormous size of the program's calculation (such proofs are callednon-surveyable proofs). Another example of a program-assisted proof is the one that shows that the game ofConnect Four can always be won by the first player.

Commercial use of automated theorem proving is mostly concentrated inintegrated circuit design and verification. Since thePentium FDIV bug, the complicatedfloating 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.^[12]

Other uses of theorem provers includeprogram synthesis, constructing programs that satisfy aformal specification.^[13] Automated theorem provers have been integrated withproof assistants, includingIsabelle/HOL.^[14]

Applications of theorem provers are also found innatural language processing andformal semantics, where they are used to analyzediscourse representations.^[15][16]

In the late 1960s agencies funding research in automated deduction began to emphasize the need for practical applications.^{[citation needed]} One of the first fruitful areas was that ofprogram verification whereby first-order theorem provers were applied to the problem of verifying the correctness of computer programs in languages such asPascal,Ada, etc. Notable among early program verification systems was the Stanford Pascal Verifier developed byDavid Luckham atStanford University.^[17][18][19] This was based on the Stanford Resolution Prover also developed at Stanford usingJohn Alan Robinson'sresolution principle. This was the first automated deduction system to demonstrate an ability to solve mathematical problems that were announced in theNotices of the American Mathematical Society before solutions were formally published.^{[citation needed]}

First-order 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 semi-decidable, and a number of sound and complete calculi have been developed, enablingfully automated systems.^[20] More expressive logics, such ashigher-order 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.^[21][22]

There is substantial overlap between first-order automated theorem provers andSMT solvers. Generally, automated theorem provers focus on supporting full first-order logic with quantifiers, whereas SMT solvers focus more on supporting various theories (interpreted predicate symbols). ATPs excel at problems with lots of quantifiers, whereas SMT solvers do well on large problems without quantifiers.^[23] The line is blurry enough that some ATPs participate in SMT-COMP, while some SMT solvers participate inCASC.^[24]

The quality of implemented systems has benefited from the existence of a large library of standardbenchmark examples—theThousands of Problems for Theorem Provers (TPTP) Problem Library^[25]—as well as from theCADE ATP System Competition (CASC), a yearly competition of first-order systems for many important classes of first-order problems.

Some important systems (all have won at least one CASC competition division) are listed below.

• E is a high-performance prover for full first-order logic, but built on apurely equational calculus, originally developed in the automated reasoning group ofTechnical University of Munich under the direction ofWolfgang Bibel, and now atBaden-Württemberg Cooperative State University inStuttgart.
• Otter, developed at theArgonne National Laboratory, is based onfirst-order resolution andparamodulation. Otter has since been replaced byProver9, which is paired withMace4.
• SETHEO is a high-performance system based on the goal-directedmodel elimination calculus, originally developed by a team under direction ofWolfgang Bibel. E and SETHEO have been combined (with other systems) in the composite theorem prover E-SETHEO.
• Vampire was originally developed and implemented atManchester University byAndrei Voronkov and Kryštof 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.^[26]
• Waldmeister is a specialized system for unit-equational first-order 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^[27] 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.

This articleis inlist format but may read better asprose. You can help byconverting this article, if appropriate.Editing help is available.(December 2023)

• First-order resolution withunification
• Model elimination
• Method of analytic tableaux
• Superposition and termrewriting
• Model checking
• Mathematical induction^[28]
• Binary decision diagrams
• DPLL
• Higher-order unification
• Quantifier elimination^[29]

• Alt-Ergo
• Automath
• CVC
• E
• IsaPlanner
• LCF
• Mizar
• NuPRL
• Paradox
• Prover9
• PVS
• SPARK (programming language)
• Twelf
• Z3 Theorem Prover

• CARINE
• Wolfram Mathematica
• ResearchCyc

• A list of theorem proving tools

• Automated theorem proving
• Formal methods

• CS1 French-language sources (fr)
• Articles with short description
• Short description is different from Wikidata
• Articles needing additional references from April 2010
• All articles needing additional references
• All articles with unsourced statements
• Articles with unsourced statements from December 2023
• Articles with unsourced statements from September 2020
• Articles needing cleanup from December 2023
• All pages needing cleanup
• Articles with sections that need to be turned into prose from December 2023