Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Automated reasoning
open-in-new
<h2 id="early-years">Early years</h2> <p>The development of <a href="/facts/Formal_logic/SaI7Y3wN">formal logic</a> played a big role in the field of automated reasoning, which itself led to the development of <a href="/facts/Artificial_intelligence/lJGauQwX">artificial intelligence</a>. A <a href="/facts/Formal_proof/6nEhV4cw">formal proof</a> is a proof in which every logical inference has been checked back to the fundamental <a href="/facts/Axioms/mLjP14Mc">axioms</a> of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive and less susceptible to logical errors.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a> </p><p>Some consider the Cornell Summer meeting of 1957, which brought together many logicians and computer scientists, as the origin of automated reasoning, or <a href="/facts/Automated_deduction/vKGvuKFI">automated deduction</a>.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> Others say that it began before that with the 1955 <a href="/facts/Logic_Theorist/cCCDAyCq">Logic Theorist</a> program of Newell, Shaw and Simon, or with Martin Davis’ 1954 implementation of <a href="/facts/Presburger_arithmetic/9R0WMG3h">Presburger's decision procedure</a> (which proved that the sum of two even numbers is even).<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a> </p><p>Automated reasoning, although a significant and popular area of research, went through an "<a href="/facts/AI_winter/DLpU1wxl">AI winter</a>" in the eighties and early nineties. The field subsequently revived, however. For example, in 2005, <a href="/facts/Microsoft/nGIDDXdx">Microsoft</a> started using <a href="/facts/Software_verification/PczD7lsh">verification technology</a> in many of their internal projects and is planning to include a logical specification and checking language in their 2012 version of Visual C.<a class="footnote-ref" id="fnref:5" href="#fn:5"><sup>5</sup></a> </p> <h2 id="significant-contributions">Significant contributions</h2> <p><a href="/facts/Principia_Mathematica/7ufeceV4">Principia Mathematica</a> was a milestone work in <a href="/facts/Formal_logic/SaI7Y3wN">formal logic</a> written by <a href="/facts/Alfred_North_Whitehead/7KuylmP3">Alfred North Whitehead</a> and <a href="/facts/Bertrand_Russell/SRpwNX2U">Bertrand Russell</a>. Principia Mathematica - also meaning <a href="/facts/Principles_of_Mathematics/Vd3bSkkt">Principles of Mathematics</a> - was written with a purpose to derive all or some of the <a href="/facts/Mathematical_expression/MPrMlYbE">mathematical expressions</a>, in terms of <a href="/facts/Symbolic_logic/SaI7Y3wN">symbolic logic</a>. Principia Mathematica was initially published in three volumes in 1910, 1912 and 1913.<a class="footnote-ref" id="fnref:6" href="#fn:6"><sup>6</sup></a> </p><p><a href="/facts/Logic_Theorist/cCCDAyCq">Logic Theorist</a> (LT) was the first ever program developed in 1956 by <a href="/facts/Allen_Newell/61yUQ647">Allen Newell</a>, <a href="/facts/Cliff_Shaw/HEKfD595">Cliff Shaw</a> and <a href="/facts/Herbert_A._Simon/NNHhQ2bS">Herbert A. Simon</a> to "mimic human reasoning" in proving theorems and was demonstrated on fifty-two theorems from chapter two of Principia Mathematica, proving thirty-eight of them.<a class="footnote-ref" id="fnref:7" href="#fn:7"><sup>7</sup></a> In addition to proving the theorems, the program found a proof for one of the theorems that was more elegant than the one provided by Whitehead and Russell. After an unsuccessful attempt at publishing their results, Newell, Shaw, and Herbert reported in their publication in 1958, <i>The Next Advance in Operation Research</i>: </p> <i>"There are now in the world machines that think, that learn and that create. Moreover, their ability to do these things is going to increase rapidly until (in a visible future) the range of problems they can handle will be co- extensive with the range to which the human mind has been applied."<a class="footnote-ref" id="fnref:8" href="#fn:8"><sup>8</sup></a> </i> <p>Examples of Formal Proofs </p> <table><tbody><tr><th>Year</th><th>Theorem</th><th>Proof System</th><th>Formalizer</th><th>Traditional Proof</th></tr><tr><td>1986</td><td><a href="/facts/Incompleteness_theorem/du8PRu8g">First Incompleteness</a></td><td><a href="/facts/Boyer-Moore_theorem_prover/8khmmL71">Boyer-Moore</a></td><td>Shankar<a class="footnote-ref" id="fnref:9" href="#fn:9"><sup>9</sup></a></td><td><a href="/facts/G%C3%B6del/P14DqKqK">Gödel</a></td></tr><tr><td>1990</td><td><a href="/facts/Quadratic_Reciprocity/leCHbu5B">Quadratic Reciprocity</a></td><td><a href="/facts/Boyer-Moore_theorem_prover/8khmmL71">Boyer-Moore</a></td><td>Russinoff<a class="footnote-ref" id="fnref:10" href="#fn:10"><sup>10</sup></a></td><td><a href="/facts/Gotthold_Eisenstein/lXTYgsU5">Eisenstein</a></td></tr><tr><td>1996</td><td><a href="/facts/Fundamental_theorem_of_calculus/pHeSGtUx">Fundamental- of Calculus</a></td><td><a href="/facts/HOL_Light/kupyFvhk">HOL Light</a></td><td>Harrison</td><td>Henstock</td></tr><tr><td>2000</td><td><a href="/facts/Fundamental_theorem_of_algebra/vspflSsM">Fundamental- of Algebra</a></td><td><a href="/facts/Mizar_system/lX1GUsUG">Mizar</a></td><td>Milewski</td><td>Brynski</td></tr><tr><td>2000</td><td><a href="/facts/Fundamental_theorem_of_algebra/vspflSsM">Fundamental- of Algebra</a></td><td><a href="/facts/Coq_(software)/7oBXgLCE">Coq</a></td><td>Geuvers et al.</td><td>Kneser</td></tr><tr><td>2004</td><td><a href="/facts/Four_color_theorem/HTS4Nway">Four Color</a></td><td><a href="/facts/Coq_(software)/7oBXgLCE">Coq</a></td><td>Gonthier</td><td><a href="/facts/Neil_Robertson_(mathematician)/nC5FXjur">Robertson</a> et al.</td></tr><tr><td>2004</td><td><a href="/facts/Prime_number_theorem/3KA9egls">Prime Number</a></td><td><a href="/facts/Isabelle_(proof_assistant)/CNbtbX83">Isabelle</a></td><td>Avigad et al.</td><td><a href="/facts/Atle_Selberg/3JDSUN2k">Selberg</a>-<a href="/facts/Paul_Erd%C5%91s/63LoUTe1">Erdős</a></td></tr><tr><td>2005</td><td><a href="/facts/Jordan_curve_theorem/zKpty4QT">Jordan Curve</a></td><td><a href="/facts/HOL_Light/kupyFvhk">HOL Light</a></td><td>Hales</td><td>Thomassen</td></tr><tr><td>2005</td><td><a href="/facts/Brouwer_fixed-point_theorem/xP2p03lQ">Brouwer Fixed Point</a></td><td><a href="/facts/HOL_Light/kupyFvhk">HOL Light</a></td><td>Harrison</td><td>Kuhn</td></tr><tr><td>2006</td><td><a href="/facts/Kepler_conjecture/5cFNDqwA">Flyspeck 1</a></td><td><a href="/facts/Isabelle_(proof_assistant)/CNbtbX83">Isabelle</a></td><td>Bauer- Nipkow</td><td>Hales</td></tr><tr><td>2007</td><td><a href="/facts/Cauchy_residue_theorem/M5ITFIyx">Cauchy Residue</a></td><td><a href="/facts/HOL_Light/kupyFvhk">HOL Light</a></td><td>Harrison</td><td>Classical</td></tr><tr><td>2008</td><td><a href="/facts/Prime_number_theorem/3KA9egls">Prime Number</a></td><td><a href="/facts/HOL_Light/kupyFvhk">HOL Light</a></td><td>Harrison</td><td>Analytic proof</td></tr><tr><td>2012</td><td><a href="/facts/Feit-Thompson_theorem/vh6D34S9">Feit-Thompson</a></td><td><a href="/facts/Coq_(software)/7oBXgLCE">Coq</a></td><td>Gonthier et al.<a class="footnote-ref" id="fnref:11" href="#fn:11"><sup>11</sup></a></td><td>Bender, Glauberman and Peterfalvi</td></tr><tr><td>2016</td><td><a href="/facts/Boolean_Pythagorean_triples_problem/WllJtAtB">Boolean Pythagorean triples problem</a></td><td>Formalized as <a href="/facts/Boolean_satisfiability_problem/wBVRjWoy">SAT</a></td><td>Heule et al.<a class="footnote-ref" id="fnref:12" href="#fn:12"><sup>12</sup></a></td><td>None</td></tr></tbody></table> <h2 id="proof-systems">Proof systems</h2> Boyer-Moore Theorem Prover (NQTHM) The design of <a href="/facts/Nqthm/8khmmL71">NQTHM</a> was influenced by John McCarthy and Woody Bledsoe. Started in 1971 at Edinburgh, Scotland, this was a fully automatic theorem prover built using Pure <a href="/facts/Lisp_(programming_language)/xJHA3CrX">Lisp</a>. The main aspects of NQTHM were: <ol><li>the use of Lisp as a working logic.</li> <li>the reliance on a principle of definition for total recursive functions.</li> <li>the extensive use of rewriting and "symbolic evaluation".</li> <li>an induction heuristic based the failure of symbolic evaluation.<a class="footnote-ref" id="fnref:13" href="#fn:13"><sup>13</sup></a><a class="footnote-ref" id="fnref:14" href="#fn:14"><sup>14</sup></a></li></ol> HOL Light Written in <a href="/facts/OCaml/ThBGLND8">OCaml</a>, <a href="/facts/HOL_Light/kupyFvhk">HOL Light</a> is designed to have a simple and clean logical foundation and an uncluttered implementation. It is essentially another proof assistant for classical higher order logic.<a class="footnote-ref" id="fnref:15" href="#fn:15"><sup>15</sup></a> Coq Developed in France, <a href="/facts/Coq_(software)/7oBXgLCE">Coq</a> is another automated proof assistant, which can automatically extract executable programs from specifications, as either Objective CAML or <a href="/facts/Haskell_(programming_language)/4Htv9WLu">Haskell</a> source code. Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC).<a class="footnote-ref" id="fnref:16" href="#fn:16"><sup>16</sup></a> <h2 id="applications">Applications</h2> <p>Automated reasoning has been most commonly used to build automated theorem provers. Oftentimes, however, theorem provers require some human guidance to be effective and so more generally qualify as <a href="/facts/Proof_assistant/hjFGxLPn">proof assistants</a>. In some cases such provers have come up with new approaches to proving a theorem. <a href="/facts/Logic_Theorist/cCCDAyCq">Logic Theorist</a> is a good example of this. The program came up with a proof for one of the theorems in <a href="/facts/Principia_Mathematica/7ufeceV4">Principia Mathematica</a> that was more efficient (requiring fewer steps) than the proof provided by Whitehead and Russell. Automated reasoning programs are being applied to solve a growing number of problems in formal logic, mathematics and computer science, <a href="/facts/Logic_programming/Xgh8lj3F">logic programming</a>, software and hardware verification, <a href="/facts/Circuit_design/wVL89XsX">circuit design</a>, and many others. The <a href="/facts/Automated_theorem_proving/vKGvuKFI">TPTP</a> (Sutcliffe and Suttner 1998) is a library of such problems that is updated on a regular basis. There is also a competition among automated theorem provers held regularly at the <a href="/facts/Conference_on_Automated_Deduction/tJCaU8T7">CADE</a> conference (Pelletier, Sutcliffe and Suttner 2002); the problems for the competition are selected from the TPTP library.<a class="footnote-ref" id="fnref:17" href="#fn:17"><sup>17</sup></a> </p> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Automated_machine_learning/7MRUSKHq">Automated machine learning</a> (AutoML)</li> <li><a href="/facts/Automated_theorem_proving/vKGvuKFI">Automated theorem proving</a></li> <li><a href="/facts/Reasoning_system/V6c6TToD">Reasoning system</a></li> <li><a href="/facts/Semantic_reasoner/rXkm48cY">Semantic reasoner</a></li> <li><a href="/facts/Program_analysis_(computer_science)/oaJTAjhH">Program analysis (computer science)</a></li> <li><a href="/facts/Applications_of_artificial_intelligence/tIeFJjMo">Applications of artificial intelligence</a></li> <li><a href="/facts/Outline_of_artificial_intelligence/gpySbMRe">Outline of artificial intelligence</a></li> <li><a href="/facts/Casuistry/3xNAPEFK">Casuistry</a> • <a href="/facts/Case-based_reasoning/JkxLXCqF">Case-based reasoning</a></li> <li><a href="/facts/Abductive_reasoning/QoHNqvKT">Abductive reasoning</a></li> <li><a href="/facts/Inference_engine/oLlNX14Q">Inference engine</a></li> <li><a href="/facts/Commonsense_reasoning/HfL7zQe4">Commonsense reasoning</a></li></ul> <h3>Conferences and workshops</h3> <ul><li><a href="/facts/International_Joint_Conference_on_Automated_Reasoning/EXE4KhUd">International Joint Conference on Automated Reasoning</a> (IJCAR)</li> <li><a href="/facts/Conference_on_Automated_Deduction/tJCaU8T7">Conference on Automated Deduction</a> (CADE)</li> <li><a href="/facts/International_Conference_on_Automated_Reasoning_with_Analytic_Tableaux_and_Related_Methods/7xYpSTI0">International Conference on Automated Reasoning with Analytic Tableaux and Related Methods</a></li></ul> <h3>Journals</h3> <ul><li><i><a href="/facts/Journal_of_Automated_Reasoning/a7e2M7CJ">Journal of Automated Reasoning</a></i></li></ul> <h3>Communities</h3> <ul><li><a href="/facts/Association_for_Automated_Reasoning/tnrw8sKl">Association for Automated Reasoning</a> (AAR)</li></ul> <h2 id="external-links">External links</h2> <ul><li><a href="https://web.archive.org/web/20090310081227/http://www.csc.liv.ac.uk/~konev/iwil2008/">International Workshop on the Implementation of Logics</a></li> <li><a href="https://web.archive.org/web/20100206221517/http://www.eprover.org/EVENTS/es_series.html">Workshop Series on Empirically Successful Topics in Automated Reasoning</a></li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997. <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.81.501&rep=rep1&type=pdf" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.81.501&rep=rep1&type=pdf</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19 <a href="https://www.ams.org/notices/200811/tx081101370p.pdf" target="_blank">https://www.ams.org/notices/200811/tx081101370p.pdf</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>"Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19 <a href="http://www.cs.cornell.edu/info/projects/nuprl/Intro/AutoDeduction/autoded.html" target="_blank">http://www.cs.cornell.edu/info/projects/nuprl/Intro/AutoDeduction/autoded.html</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Martin Davis (1983). "The Prehistory and Early History of Automated Deduction". In Jörg Siekmann; G. Wrightson (eds.). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. pp. 1–28. ISBN 978-3-642-81954-4. Here: p.15 <a href="978-3-642-81954-4" target="_blank">978-3-642-81954-4</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>"Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19 <a href="http://www.cs.cornell.edu/info/projects/nuprl/Intro/AutoDeduction/autoded.html" target="_blank">http://www.cs.cornell.edu/info/projects/nuprl/Intro/AutoDeduction/autoded.html</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>"Principia Mathematica", at Stanford University. Retrieved 2010-10-19 <a href="http://plato.stanford.edu/entries/principia-mathematica/" target="_blank">http://plato.stanford.edu/entries/principia-mathematica/</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>"The Logic Theorist and its Children". Retrieved 2010-10-18 <a href="http://www.cs.swarthmore.edu/~eroberts/cs91/projects/ethics-of-ai/sec1_2.html" target="_blank">http://www.cs.swarthmore.edu/~eroberts/cs91/projects/ethics-of-ai/sec1_2.html</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19 <a href="http://www.csl.sri.com/~shankar/" target="_blank">http://www.csl.sri.com/~shankar/</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> <li id="fn:9"><p>Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, ISBN 9780521585330 <a href="9780521585330" target="_blank">9780521585330</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li> <li id="fn:10"><p>Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446, S2CID 14824949 <a href="/wiki/Doi_(identifier)" target="_blank">/wiki/Doi_(identifier)</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></p></li> <li id="fn:11"><p>Gonthier, G.; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem" (PDF), in Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (eds.), Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 7998, pp. 163–179, CiteSeerX 10.1.1.651.7964, doi:10.1007/978-3-642-39634-2_14, ISBN 978-3-642-39633-5, S2CID 1855636 <a href="978-3-642-39633-5" target="_blank">978-3-642-39633-5</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></p></li> <li id="fn:12"><p>Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer". Theory and Applications of Satisfiability Testing – SAT 2016. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6. S2CID 7912943. <a href="978-3-319-40969-6" target="_blank">978-3-319-40969-6</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></p></li> <li id="fn:13"><p>The Boyer-Moore Theorem Prover Retrieved on 2010-10-23 <a href="http://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html" target="_blank">http://www.cs.utexas.edu/~moore/best-ideas/nqthm/index.html</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></p></li> <li id="fn:14"><p>Boyer, Robert S. and Moore, J Strother and Passmore, Grant Olney The PLTP Archive. Retrieved on 2023-07-27 <a href="https://www.cs.utexas.edu/users/moore/best-ideas/pltp/index.html" target="_blank">https://www.cs.utexas.edu/users/moore/best-ideas/pltp/index.html</a> <a href="#fnref:14" class="footnote-back-ref">↩</a></p></li> <li id="fn:15"><p>Harrison, John HOL Light: an overview. Retrieved 2010-10-23 <a href="http://www.cl.cam.ac.uk/~jrh13/slides/tphols-18aug09/slides.pdf" target="_blank">http://www.cl.cam.ac.uk/~jrh13/slides/tphols-18aug09/slides.pdf</a> <a href="#fnref:15" class="footnote-back-ref">↩</a></p></li> <li id="fn:16"><p>Introduction to Coq. Retrieved 2010-10-23 <a href="http://coq.inria.fr/a-short-introduction-to-coq" target="_blank">http://coq.inria.fr/a-short-introduction-to-coq</a> <a href="#fnref:16" class="footnote-back-ref">↩</a></p></li> <li id="fn:17"><p>Automated Reasoning, Stanford Encyclopedia. Retrieved 2010-10-10 <a href="http://plato.stanford.edu/entries/reasoning-automated/" target="_blank">http://plato.stanford.edu/entries/reasoning-automated/</a> <a href="#fnref:17" class="footnote-back-ref">↩</a></p></li> </ol>