Automated reasoning
In
The most developed subareas of automated reasoning are
Other important topics include
Tools and techniques of automated reasoning include the classical logics and calculi, fuzzy logic, Bayesian inference, reasoning with maximal entropy and many less formal ad hoc techniques.
Early years
The development of
Some consider the Cornell Summer meeting of 1957, which brought together many logicians and computer scientists, as the origin of automated reasoning, or
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 using verification 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.[4]
Significant contributions
Logic Theorist (LT) was the first ever program developed in 1956 by Allen Newell, Cliff Shaw and Herbert 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.[7] 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:
- "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."[8]
Examples of Formal Proofs
Year Theorem Proof System Formalizer Traditional Proof 1986 First IncompletenessBoyer-MooreShankar[9] Gödel1990 Quadratic ReciprocityBoyer-MooreRussinoff[10] 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 ResidueHOL Light Harrison Classical 2008 Prime Number HOL Light Harrison Analytic proof 2012 Feit-ThompsonCoq Gonthier et al.[11] Bender, Glauberman and Peterfalvi 2016 Boolean Pythagorean triples problem Formalized as SAT Heule et al.[12] None
Proof systems
- Boyer-Moore Theorem Prover (NQTHM)
- The design of NQTHM was influenced by John McCarthy and Woody Bledsoe. Started in 1971 at Edinburgh, Scotland, this was a fully automatic theorem prover built using Pure Lisp. The main aspects of NQTHM were:
- HOL Light
- Written in OCaml, HOL Light 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.[15]
- Coq
- Developed in France, Haskell source code. Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC).[16]
Applications
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 proof 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 in Principia 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. The TPTP (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 CADE conference (Pelletier, Sutcliffe and Suttner 2002); the problems for the competition are selected from the TPTP library.[17]
See also
- Automated machine learning (AutoML)
- Automated theorem proving
- Reasoning system
- Semantic reasoner
- Program analysis (computer science)
- Applications of artificial intelligence
- Outline of artificial intelligence
- Casuistry • Case-based reasoning
- Abductive reasoning
- Inference engine
- Commonsense reasoning
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
Journals
Communities
References
- ^ Defourneaux, Gilles, and Nicolas Peltier. "Analogy and abduction in automated deduction." IJCAI (1). 1997.
- ^ John L. Pollock[full citation needed]
- ^ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
- ^ a b "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
- ISBN 978-3-642-81954-4. Here: p.15
- ^ "Principia Mathematica", at Stanford University. Retrieved 2010-10-19
- ^ "The Logic Theorist and its Children". Retrieved 2010-10-18
- ^ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, SRI International. Retrieved 2010-10-19
- ISBN 9780521585330
- S2CID 14824949
- S2CID 1855636
- S2CID 7912943.
- ^ The Boyer-Moore Theorem Prover Retrieved on 2010-10-23
- ^ Boyer, Robert S. and Moore, J Strother and Passmore, Grant Olney The PLTP Archive. Retrieved on 2023-07-27
- ^ Harrison, John HOL Light: an overview. Retrieved 2010-10-23
- ^ Introduction to Coq. Retrieved 2010-10-23
- Stanford Encyclopedia. Retrieved 2010-10-10