Editing Automated theorem proving (section)

== Logical foundations ==
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>

In 1929, [[Mojżesz Presburger]] showed that the [[first-order theory]] of the [[natural numbers]] with addition and equality (now called [[Presburger arithmetic]] in his honor) is [[Decidability (logic)|decidable]] and gave an algorithm that could determine if a given [[sentence (logic)|sentence]] in the [[language (logic)|language]] was true or false.<ref>{{cite journal|last=Presburger|first=Mojżesz|title=Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt|journal=Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves|year=1929|pages=92–101|location=Warszawa}}</ref><ref name=Davis2001>{{Cite book
| last = Davis
| first = Martin
| author-link = Martin Davis (mathematician)
| chapter = The Early History of Automated Deduction
| year = 2001
| chapter-url = http://cs.nyu.edu/cs/faculty/davism/early.ps
| title = {{harvnb|Robinson|Voronkov|2001}}
| access-date = 2012-09-08
| archive-date = 2012-07-28
| archive-url = https://web.archive.org/web/20120728092819/http://www.cs.nyu.edu/cs/faculty/davism/early.ps
| url-status = dead
}}</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.