Automated reasoning

Automated reasoning is an area of computer science dedicated to understanding different aspects of reasoning in a way that allows the creation of software which allows computers to reason completely or nearly completely, automatically. As such, it is usually considered a subfield of artificial intelligence, but it also has strong connections to theoretical computer science and even philosophy.

The most developed subareas of automated reasoning probably are automated theorem proving (and the less automated but more pragmatic subfield of interactive theorem proving) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions), but extensive work has also been done in reasoning by analogy induction and abduction. Other important topics are reasoning under uncertainty and non-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 include the classical logics and calculi from automated theorem proving, but also fuzzy logic, Bayesian inference, reasoning with maximal entropy and a large number of less formal ad-hoc techniques.

Early Years

The development of formal logic played a big role in the field of automated reasoning which itself led to the development of Artificial Intelligence. A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms 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.

Together the advent of the computer era and development of formal proofs attracted mathematicians, logicians and computer scientists to research and develop computer aided assistance to proof mathematical and logical expressions using formal proofs. Some consider the Cornell Summer meeting of 1957 as the origin of the automated reasoning or automated deduction which brought together a large number of logicians and computer scientists. Other say that it began before that with the 1955 Logic Theorist program of Newell, Shaw and Simon, or with Martin Davis’ 1954 implementation of Presburger’s decision procedure (which proved that the sum of two even numbers is even). Automated reasoning, although significant and popular area of research in the eighties and early nineties was left for dead. Amazingly, in 2005, Microsoft is now using verification technology in many of their internal projects and is currently planning to include a logical specification and checking language in their next version of Visual C.

Significant Contributions

• Principia Mathematica was a milestone work in formal logic written by Alfred North Whitehead and Bertrand Russell. Principia Mathematica also meaning Principles of Mathematics was written with a purpose to derive all or some of the mathematical expressions, in terms of symbolic logic. Principia Mathematica was initially published in three volumes each in 1910, 1912 and 1913.

• Logic Theorist (LT) was the first ever program developed in 1956 by Allen Newell, Cliff Shaw and Herbert Simon to "mimic human reasoning" in proving theorems and was demonstrated on fifty- two theorems from chapter two of Principia Mathematica written by Whitehead and Russell. LT proved thirty eight of them . Besides proving the theorems, the program found a proof for one of the theorems which was more elegant than the one provided by Whitehead and Russel. After unsuccessful attempt of publishing their results Newell, Shaw and Herbert reported in their publication in 1958: The Next Advance in Operation Research:

There are now in the world machines that think, that learn and that create.

Moreover, their ability to do there 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 .

• Examples of Formal Proofs

Year	Theorem	Proof System	Formalizer	Traditional Proof
1986	First Incompleteness	Boyer- Moore	Shankar	Godel
1990	Quadratic Reciprocity	Boyer- Moore	Russinoff	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-Erdos
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

See also

• Automated theorem proving
• Program analysis (computer science)
• Automated deduction

Conferences and workshops

• International Joint Conference on Automated Reasoning (IJCAR)
• Conference on Automated Deduction (CADE)
• International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
• International Workshop on the Implementation of Logics
• Workshop Series on Empirically Successful Topics in Automated Reasoning

Journals

• Journal of Automated Reasoning

Communities

• Association for Automated Reasoning (AAR)