Automated theorem proving: Difference between revisions

While the roots of formalized [[Logicism|logic]] go back to [[Aristotelian logic|Aristotle]], the end of the 19th and early 20th centuries saw the development of modern logic and formalized mathematics. [[Gottlob Frege|Frege]]'s ''[[Begriffsschrift]]'' (1879) introduced both a complete [[propositional logic|propositional calculus]] and what is essentially modern [[predicate logic]].<ref>{{cite book|last=Frege|first=Gottlob|title=Begriffsschrift|year=1879|publisher=Verlag Louis Neuert|url=http://gallica.bnf.fr/ark:/12148/bpt6k65658c}}</ref> His ''[[The Foundations of Arithmetic|Foundations of Arithmetic]]'', published in 1884,<ref>{{cite book|last=Frege|first=Gottlob|title=Die Grundlagen der Arithmetik|year=1884|publisher=Wilhelm Kobner|location=Breslau|url=http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|access-date=2012-09-02|archive-url=https://web.archive.org/web/20070926172317/http://www.ac-nancy-metz.fr/enseign/philo/textesph/Frege.pdf|archive-date=2007-09-26|url-status=dead}}</ref> expressed (parts of) mathematics in formal logic. This approach was continued by [[Bertrand Russell|Russell]] and [[Alfred North Whitehead|Whitehead]] in their influential ''[[Principia Mathematica]]'', first published 1910–1913,<ref>{{cite book |author=Russell |first1=Bertrand |url=https://archive.org/details/cu31924001575244 |title=Principia Mathematica |last2=Whitehead |first2=Alfred North |publisher=Cambridge University Press |year=1910–1913 |edition=1st}}</ref> and with a revised second edition in 1927.<ref>{{cite book |author=Russell |first1=Bertrand |url=https://archive.org/details/in.ernet.dli.2015.221192 |title=Principia Mathematica |last2=Whitehead |first2=Alfred North |publisher=Cambridge University Press |year=1927 |edition=2nd |language=en}}</ref> Russell and Whitehead thought they could derive all mathematical truth using [[axiom]]s and [[inference rule]]s of formal logic, in principle opening up the process to automation. 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 [[satisfiability|(un)satisfiability]] of first-order formulas (and hence the [[Validity (logic)|validity]] of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.<ref>{{cite thesis |first=J. |last=Herbrand |title=Recherches sur la théorie de la démonstration |date=1930 |type=PhD |publisher=University of Paris |url=https://eudml.org/doc/192791 |language=fr}}</ref>

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 that 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 of [[Undecidable problem|undecidable question]]s.

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the common case of [[propositional logic]], the problem is decidable but [[co-NP-complete]], and hence only [[exponential time|exponential-time]] algorithms are believed to exist for general proof tasks. For a [[first-order logic|first-order predicate calculus]], [[Gödel's completeness theorem]] states that the theorems (provable statements) are exactly the semantically valid [[well-formed formula]]s, so the valid formulas are [[computably 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 axioms|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 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 the [[integer]]s).

Commercial use of automated theorem proving is mostly concentrated in [[integrated circuit design]] and verification. Since the [[Pentium FDIV bug]], the complicated [[floating point unit]]s 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.<ref>{{Citation |last=Goel |first=Shilpi |title=Microprocessor Assurance and the Role of Theorem Proving |date=2022 |work=Handbook of Computer Architecture |pages=1–43 |editor-last=Chattopadhyay |editor-first=Anupam |url=https://link.springer.com/10.1007/978-981-15-6401-7_38-1 |access-date=2024-02-10 |place=Singapore |publisher=Springer Nature Singapore |language=en |doi=10.1007/978-981-15-6401-7_38-1 |isbn=978-981-15-6401-7 |last2=Ray |first2=Sandip|url-access=subscription }}</ref>

* [[Vampire theorem prover|Vampire]] was originally developed and implemented at [[University of Manchester|Manchester University]] by [[Andrei 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.<ref>{{cite web |title=History |url=https://vprover.github.io/history.html |website=vprover.github.io}}</ref>