Automated reasoning
Encyclopedia
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.
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.
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. 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). 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.
|-
! 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
|}
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:
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.
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).
(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.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
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
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
it also has connections with theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
and even philosophy
Philosophy
Philosophy is the study of general and fundamental problems, such as those connected with existence, knowledge, values, reason, mind, and language. Philosophy is distinguished from other ways of addressing such problems by its critical, generally systematic approach and its reliance on rational...
.
The most developed subareas of automated reasoning are automated theorem proving
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
(and the less automated but more pragmatic subfield of interactive theorem proving
Interactive theorem proving
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...
) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions). Extensive work has also been done in reasoning by analogy
Analogy
Analogy is a cognitive process of transferring information or meaning from a particular subject to another particular subject , and a linguistic expression corresponding to such a process...
induction and abduction
Abductive reasoning
Abduction is a kind of logical inference described by Charles Sanders Peirce as "guessing". The term refers to the process of arriving at an explanatory hypothesis. Peirce said that to abduce a hypothetical explanation a from an observed surprising circumstance b is to surmise that a may be true...
. Other important topics are reasoning under uncertainty
Uncertainty
Uncertainty is a term used in subtly different ways in a number of fields, including physics, philosophy, statistics, economics, finance, insurance, psychology, sociology, engineering, and information science...
and non-monotonic
Non-monotonic logic
A non-monotonic logic is a formal logic whose consequence relation is not monotonic. Most studied formal logics have a monotonic consequence relation, meaning that adding a formula to a theory never produces a reduction of its set of consequences. Intuitively, monotonicity indicates that learning a...
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
Fuzzy logic
Fuzzy logic is a form of many-valued logic; it deals with reasoning that is approximate rather than fixed and exact. In contrast with traditional logic theory, where binary sets have two-valued logic: true or false, fuzzy logic variables may have a truth value that ranges in degree between 0 and 1...
, Bayesian inference
Bayesian inference
In statistics, Bayesian inference is a method of statistical inference. It is often used in science and engineering to determine model parameters, make predictions about unknown variables, and to perform model selection...
, reasoning with maximal entropy and a large number of less formal ad-hoc techniques.
Early years
The development of formal logicFormal logic
Classical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
played a big role in the field of automated reasoning which itself led to the development of Artificial Intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
. A formal proof
Formal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
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.
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. Others say that it began before that with the 1955 Logic Theorist
Logic Theorist
Logic Theorist is a computer program written in 1955 and 1956 by Allen Newell, Herbert Simon and J. C. Shaw. It was the first program deliberately engineered to mimic the problem solving skills of a human being and is called "the first artificial intelligence program." It would eventually prove 38...
program of Newell, Shaw and Simon, or with Martin Davis’ 1954 implementation of Presburger’s decision procedure
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
(which proved that the sum of two even numbers is even). Automated reasoning, although a significant and popular area of research, went through an "AI winter
AI winter
In the history of artificial intelligence, an AI winter is a period of reduced funding and interest in artificial intelligence research. The process of hype, disappointment and funding cuts are common in many emerging technologies , but the problem has been particularly acute for AI...
" in the eighties and early nineties. Luckily, it got revived after that. For example, in 2005, Microsoft
Microsoft
Microsoft Corporation is an American public multinational corporation headquartered in Redmond, Washington, USA that develops, manufactures, licenses, and supports a wide range of products and services predominantly related to computing through its various product divisions...
started using verification technology
Software verification
Software verification is a broader and more complex discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements.There are two fundamental approaches to verification:...
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 MathematicaPrincipia MathematicaThe Principia Mathematica is a three-volume work on the foundations of mathematics, written by Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913...
was a milestone work in formal logicFormal logicClassical or traditional system of determining the validity or invalidity of a conclusion deduced from two or more statements...
written by Alfred North WhiteheadAlfred North WhiteheadAlfred North Whitehead, OM FRS was an English mathematician who became a philosopher. He wrote on algebra, logic, foundations of mathematics, philosophy of science, physics, metaphysics, and education...
and Bertrand RussellBertrand RussellBertrand Arthur William Russell, 3rd Earl Russell, OM, FRS was a British philosopher, logician, mathematician, historian, and social critic. At various points in his life he considered himself a liberal, a socialist, and a pacifist, but he also admitted that he had never been any of these things...
. 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 TheoristLogic TheoristLogic Theorist is a computer program written in 1955 and 1956 by Allen Newell, Herbert Simon and J. C. Shaw. It was the first program deliberately engineered to mimic the problem solving skills of a human being and is called "the first artificial intelligence program." It would eventually prove 38...
(LT) was the first ever program developed in 1956 by Allen NewellAllen NewellAllen Newell was a researcher in computer science and cognitive psychology at the RAND corporation and at Carnegie Mellon University’s School of Computer Science, Tepper School of Business, and Department of Psychology...
, Cliff ShawCliff ShawJ.C. Shaw was a systems programmer at the RAND Corporation. He is a coauthor of the first artificial intelligence program, the Logic Theorist, and was one of the developers of Information Processing Language, a programming language of the 1950s. It is considered the true "father" of the JOSS...
and Herbert SimonHerbert SimonHerbert Alexander Simon was an American political scientist, economist, sociologist, and psychologist, and professor—most notably at Carnegie Mellon University—whose research ranged across the fields of cognitive psychology, cognitive science, computer science, public administration, economics,...
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
-
-
- {| class="wikitable"
-
|-
! 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
Lisp
A lisp is a speech impediment, historically also known as sigmatism. Stereotypically, people with a lisp are unable to pronounce sibilants , and replace them with interdentals , though there are actually several kinds of 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.
-
- HOL Light
Written in Objective CAML
Objective Caml
OCaml , originally known as Objective Caml, is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996...
, 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.
- Coq
Developed in France, Coq
Coq
In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
is another automated proof assistant, which can automatically extract executable programs from specifications, as either Objective CAML or Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
source code. Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC).
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 TPTPTPTP
TPTP is an abbreviation and may refer to* Thousands of Problems for Theorem Provers* Test & Performance Tools Platform, a platform of Eclipse...
(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
Cade
Cade may refer to:* Cade an important sire of Thoroughbred racehorses.* Juniperus oxycedrus, also called the Prickly JuniperPeople with the surname Cade:* Elsa Salazar Cade, entomologist and educator* Jack Cade , English rebel...
conference (Pelletier, Sutcliffe and Suttner 2002); the problems for the competition are selected from the TPTP library.
Conferences and workshops
- International Joint Conference on Automated ReasoningInternational Joint Conference on Automated ReasoningInternational Joint Conference on Automated Reasoning 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...
(IJCAR) - Conference on Automated DeductionConference on Automated DeductionThe Conference on Automated Deduction is the premier academic conference on automated deduction and related fields. The first CADE was organized in 1974 at the Argonne National Laboratory near Chicago. Most CADE meetings have been held in Europe and the USA. However, conferences have been held all...
(CADE) - International Conference on Automated Reasoning with Analytic Tableaux and Related MethodsInternational Conference on Automated Reasoning with Analytic Tableaux and Related MethodsThe International Conference on Automated Reasoning with Analytic Tableaux and Related Methods is an annual international academic conference that deals with all aspects of automated reasoning with analytic tableaux. Periodically, it joins with CADE and TPHOLs into the International Joint...
- International Workshop on the Implementation of Logics
- Workshop Series on Empirically Successful Topics in Automated Reasoning
Communities
- Association for Automated ReasoningAssociation for Automated ReasoningThe Association for Automated Reasoning 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 publishes a roughly quarterly newsletter....
(AAR)