Automated reasoning


Automated reasoning

Automated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence it also has connections with theoretical computer science and even philosophy.

The most developed subareas of automated reasoning 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). 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 of automated reasoning include the classical logics and calculi, fuzzy logic, Bayesian inference, reasoning with maximal entropy and a large number of less formal ad-hoc techniques.

Contents

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.[1]

Some consider the Cornell Summer meeting of 1957, which brought together a large number of logicians and computer scientists, as the origin of automated reasoning, or automated deduction.[2] Others 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)[citation needed]. Automated reasoning, although a significant and popular area of research, went through an "AI winter" in the eighties and early nineties. Luckily, it got revived after that. For example, in 2005, Microsoft started 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.[2]

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.[3]
  • 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.[4] 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."[5]
  • 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

Proof systems

  • Boyer-Moore Theorem Prover (NQTHM)

The design of this system 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:

1. the use of Lisp as a working logic.
2. the reliance on a principle of definition for total recursive functions.
3. the extensive use of rewriting and "symbolic evaluation".
4. an induction heuristic based the failure of symbolic evaluation.[6]
  • HOL Light

Written in Objective CAML, 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.[7]

  • Coq

Developed in France, Coq is another automated proof assistant, which can automatically extract executable programs from specifications, as either Objective CAML or Haskell source code. Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC).[8]

Applications

Automated reasoning has been most commonly used to build automated theorem provers. 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 which was more efficient (less number of steps for solving a theorem) than the one provided by Whitehead and Russel. 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, "Automated Reasoning. 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.[9]

See also

References

  1. ^ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19
  2. ^ a b "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19
  3. ^ "Principia Mathematica".Retrieved on 2010-10-19
  4. ^ "The Logic Theorist and its Children". Retrieved 2010-10-18
  5. ^ Shankar, Natarajan "Little Engines of Proof" Computer Science Laboratory, SRI International. Retrieved 2010-10-19
  6. ^ "The Boyer- Moore Theorem Prover". Retrieved on 2010-10-23
  7. ^ Harrison, John "HOL Light: an overview". Retrieved on 2010-10-23
  8. ^ A Short Introduction to Coq "Introduction to Coq". Retrieved 2010-10-23
  9. ^ "Automated Reasoning" , "Stanford Encyclopedia". Retrieved on 2010-10-10

External links

Conferences and workshops

Journals

  • Journal of Automated Reasoning

Communities


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Mathematics Mechanization and Automated Reasoning Platform — Original author(s) 中国科学院数学机械化重点实验室 Developer(s) 中國 国家基础研究发展规划项目 数学机械化与自动推理平台 软件开发课题组 Stable release 3.0 / April 1, 2006; 5 years ago (2006 04 01) …   Wikipedia

  • International Conference on Automated Reasoning with Analytic Tableaux and Related Methods — The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it… …   Wikipedia

  • Association for Automated Reasoning — The Association for Automated Reasoning (AAR) is a non profit corporation that serves as an association of researchers working on automated theorem proving, automated reasoning, and related fields. It organizes the CADE and IJCAR conferences and… …   Wikipedia

  • Handbook of Automated Reasoning — The Handbook of Automated Reasoning (ISBN 0444508139, 2128 pages) is a collection of survey articles on the field of automated reasoning. Published on June 2001 by MIT Press, it is edited by John Alan Robinson and Andrei Voronkov. Volume 1… …   Wikipedia

  • International Joint Conference on Automated Reasoning — IJCAR is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place …   Wikipedia

  • Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia

  • Reasoning — is the cognitive process of looking for reasons for beliefs, conclusions, actions or feelings. [ Kirwin, Christopher. 1995. Reasoning . In Ted Honderich (ed.), The Oxford Companion to Philosophy . Oxford: Oxford University Press: p. 748] Humans… …   Wikipedia

  • reasoning — Any process of drawing a conclusion from a set of premises may be called a process of reasoning. If the conclusion concerns what to do, the process is called practical reasoning, otherwise pure or theoretical reasoning. Evidently such processes… …   Philosophy dictionary

  • Automated Valuation Model — (AVM) is the name given to a service that can provide property valuations using mathematical modelling combined with a database. Most AVMs calculate a property’s value at a specific point in time by analysing values of comparable properties. As… …   Wikipedia

  • automated machine-controlled machine-driven — Automatic Au to*mat ic, Automatical Au to*mat ic*al, a. [Cf. F. automatique. See {Automaton}.] 1. Having an inherent power of action or motion. [1913 Webster] Nothing can be said to be automatic. Sir H. Davy. [1913 Webster] 2. Pertaining to, or… …   The Collaborative International Dictionary of English