Incomputer science, in particular inknowledge representation and reasoning andmetalogic, the area ofautomated reasoning is dedicated to understanding different aspects ofreasoning. The study of automated reasoning helps producecomputer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field ofartificial intelligence, it also has connections withtheoretical computer science andphilosophy.
The most developed subareas of automated reasoning areautomated theorem proving (and the less automated but more pragmatic subfield ofinteractive theorem proving) andautomated proof checking (viewed as guaranteed correct reasoning under fixed assumptions).[citation needed] Extensive work has also been done in reasoning byanalogy usinginduction andabduction.[1]
Other important topics includereasoning under uncertainty andnon-monotonic reasoning. An important part of the uncertainty field is that of argumentation, where further constraints of minimality and consistency are applied on top of the more standard automated deduction.John Pollock's OSCAR system is an example of an automated argumentation system that is more specific than being just an automated theorem prover.
Tools and techniques of automated reasoning include theclassical logics and calculi,fuzzy logic,Bayesian inference, reasoning withmaximal entropy and many less formalad hoc techniques.
The development offormal logic played a big role in the field of automated reasoning, which itself led to the development ofartificial intelligence. Aformal proof is a proof in which every logical inference has been checked back to the fundamentalaxioms 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.[2]
Some consider the Cornell Summer meeting of 1957, which brought together many logicians and computer scientists, as the origin of automated reasoning, orautomated deduction.[3] Others say that it began before that with the 1955Logic Theorist program of Newell, Shaw and Simon, or with Martin Davis’ 1954 implementation ofPresburger's decision procedure (which proved that the sum of two even numbers is even).[4]
Automated reasoning, although a significant and popular area of research, went through an "AI winter" in the eighties and early nineties. The field subsequently revived, however. For example, in 2005,Microsoft started usingverification technology in many of their internal projects and is planning to include a logical specification and checking language in their 2012 version of Visual C.[3]
Principia Mathematica was a milestone work informal logic written byAlfred North Whitehead andBertrand Russell. Principia Mathematica - also meaningPrinciples of Mathematics - was written with a purpose to derive all or some of themathematical expressions, in terms ofsymbolic logic. Principia Mathematica was initially published in three volumes in 1910, 1912 and 1913.[5]
Logic Theorist (LT) was the first ever program developed in 1956 byAllen Newell,Cliff Shaw andHerbert A. Simon 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.[6] 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,The Next Advance in Operation Research:
Examples of Formal Proofs
| Year | Theorem | Proof System | Formalizer | Traditional Proof |
|---|---|---|---|---|
| 1986 | First Incompleteness | Boyer-Moore | Shankar[8] | Gödel |
| 1990 | Quadratic Reciprocity | Boyer-Moore | Russinoff[9] | Eisenstein |
| 1996 | Fundamental- of Calculus | HOL Light | Harrison | Henstock |
| 2000 | Fundamental- of Algebra | Mizar | Milewski | Brynski |
| 2000 | Fundamental- of Algebra | Coq | Geuvers et al. | Kneser |
| 2004 | Four Color | Coq | Gonthier | Robertson et al. |
| 2004 | Prime Number | Isabelle | Avigad et al. | Selberg-Erdős |
| 2005 | Jordan Curve | HOL Light | Hales | Thomassen |
| 2005 | Brouwer Fixed Point | HOL Light | Harrison | Kuhn |
| 2006 | Flyspeck 1 | Isabelle | Bauer- Nipkow | Hales |
| 2007 | Cauchy Residue | HOL Light | Harrison | Classical |
| 2008 | Prime Number | HOL Light | Harrison | Analytic proof |
| 2012 | Feit-Thompson | Coq | Gonthier et al.[10] | Bender, Glauberman and Peterfalvi |
| 2016 | Boolean Pythagorean triples problem | Formalized asSAT | Heule et al.[11] | None |
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 asproof assistants. In some cases such provers have come up with new approaches to proving a theorem.Logic Theorist is a good example of this. The program came up with a proof for one of the theorems inPrincipia Mathematica 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,logic programming, software and hardware verification,circuit design, and many others. TheTPTP (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 theCADE conference (Pelletier, Sutcliffe and Suttner 2002); the problems for the competition are selected from the TPTP library.[16]