Editing Automated theorem proving (section)

== First implementations ==

In 1954, [[Martin Davis (mathematician)|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".<ref name=Davis2001/><ref name=Bibel2007>{{cite journal|last=Bibel|first=Wolfgang|title=Early History and Perspectives of Automated Deduction|journal=Ki 2007|year=2007|series=LNAI|issue=4667|pages=2–18|url=http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.intellektik.de/resources/OsnabrueckBuchfassung.pdf |archive-date=2022-10-09 |url-status=live|access-date=2 September 2012|publisher=Springer}}</ref> More ambitious was the [[Logic Theorist]] in 1956, a deduction system for the [[propositional logic]] of the ''Principia Mathematica'', developed by [[Allen Newell]], [[Herbert A. Simon]] and [[Cliff Shaw|J. 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) [[Substitution_(logic)|variable substitution]], and the replacement of formulas by their definition. The system used [[Heuristic (computer science)|heuristic]] guidance, and managed to prove 38 of the first 52 theorems of the ''Principia''.<ref name=Davis2001/>

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 (logic)|completeness]] for first-order logic. Initial approaches relied on the results of [[Jacques Herbrand|Herbrand]] and [[Thoralf Skolem|Skolem]] to convert a first-order formula into successively larger sets of [[propositional formula]]e by instantiating variables with [[term (logic)|term]]s 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.<ref name=Davis2001/><ref>{{cite journal|last=Gilmore|first=Paul|title=A proof procedure for quantification theory: its justification and realisation|journal=IBM Journal of Research and Development|year=1960|volume=4|pages=28–35|doi=10.1147/rd.41.0028}}</ref>