In
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, in particular in
knowledge representation and reasoning
Knowledge representation (KR) aims to model information in a structured manner to formally represent it as knowledge in knowledge-based systems whereas knowledge representation and reasoning (KRR, KR&R, or KR²) also aims to understand, reason, and ...
and
metalogic, the area of automated reasoning is dedicated to understanding different aspects of
reasoning
Reason is the capacity of consciously applying logic by drawing valid conclusions from new or existing information, with the aim of seeking the truth. It is associated with such characteristically human activities as philosophy, religion, scien ...
. The study of automated reasoning helps produce
computer programs
A computer program is a sequence or set of instructions in a programming language for a computer to Execution (computing), execute. It is one component of software, which also includes software documentation, documentation and other intangibl ...
that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of
artificial intelligence
Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...
, it also has connections with
theoretical computer science
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
and
philosophy
Philosophy ('love of wisdom' in Ancient Greek) is a systematic study of general and fundamental questions concerning topics like existence, reason, knowledge, Value (ethics and social sciences), value, mind, and language. It is a rational an ...
.
The most developed subareas of automated reasoning are
automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
(and the less automated but more pragmatic subfield of
interactive theorem proving) and
automated proof checking
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 human–machine collaboration. This involves some sort of interactive proof edi ...
(viewed as guaranteed correct reasoning under fixed assumptions). Extensive work has also been done in reasoning by
analogy using
induction and
abduction.
Other important topics include
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 logic
Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this c ...
s and calculi,
fuzzy logic
Fuzzy logic is a form of many-valued logic in which the truth value of variables may be any real number between 0 and 1. It is employed to handle the concept of partial truth, where the truth value may range between completely true and completely ...
,
Bayesian inference, reasoning with
maximal entropy and many less formal ''ad hoc'' techniques.
In the 2020s, to enhance the ability of
large language models
A large language model (LLM) is a language model trained with Self-supervised learning, self-supervised machine learning on a vast amount of text, designed for natural language processing tasks, especially Natural language generation, language g ...
to solve complex problems, AI researchers have designed
reasoning language models that can spend additional time on the problem before generating an answer.
Early years
The development of
formal logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
played a big role in the field of automated reasoning, which itself led to the development of
artificial intelligence
Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...
. A
formal proof
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the s ...
is a proof in which every logical inference has been checked 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 many logicians and computer scientists, as the origin of automated reasoning, or
automated deduction.
["Automated Deduction (AD)"](_blank)
'' he Nature of PRL Project'. Retrieved on 2010-10-19 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. The field subsequently revived, however. For example, in 2005,
Microsoft
Microsoft Corporation is an American multinational corporation and technology company, technology conglomerate headquartered in Redmond, Washington. Founded in 1975, the company became influential in the History of personal computers#The ear ...
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.
Significant contributions
Principia Mathematica
The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by the mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1 ...
was a milestone work in
formal logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
written by
Alfred North Whitehead
Alfred North Whitehead (15 February 1861 – 30 December 1947) was an English mathematician and philosopher. He created the philosophical school known as process philosophy, which has been applied in a wide variety of disciplines, inclu ...
and
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British philosopher, logician, mathematician, and public intellectual. He had influence on mathematics, logic, set theory, and various areas of analytic ...
. Principia Mathematica - also meaning
Principles of Mathematics - was written with a purpose to derive all or some of the
mathematical expression
In mathematics, an expression is a written arrangement of symbols following the context-dependent, syntactic conventions of mathematical notation. Symbols can denote numbers, variables, operations, and functions. Other symbols include punct ...
s, in terms of
symbolic logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
. Principia Mathematica was initially published in three volumes in 1910, 1912 and 1913.
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. 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." ''
Examples of Formal Proofs
:
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
Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation.
Originally specified in the late 1950s, ...
. The main aspects of NQTHM were:
:# the use of Lisp as a working logic.
:# the reliance on a principle of definition for total recursive functions.
:# the extensive use of rewriting and "symbolic evaluation".
:# an induction heuristic based the failure of symbolic evaluation.
;HOL Light
:Written in
OCaml
OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...
,
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 is another automated proof assistant, which can automatically extract executable programs from specifications, as either Objective CAML or
Haskell
Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
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. 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
The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by the mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1 ...
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
Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
, 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.
See also
*
Automated machine learning (AutoML)
*
Automated theorem proving
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...
*
Reasoning system
*
Semantic reasoner
*
Program analysis (computer science)
*
Applications of artificial intelligence
*
Outline of artificial intelligence
*
Casuistry •
Case-based reasoning
*
Abductive reasoning
Abductive reasoning (also called abduction,For example: abductive inference, or retroduction) is a form of logical inference that seeks the simplest and most likely conclusion from a set of observations. It was formulated and advanced by Ameri ...
*
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
* ''
Journal of Automated Reasoning''
Communities
*
Association for Automated Reasoning (AAR)
References
External links
International Workshop on the Implementation of Logics
{{Automated reasoning
Theoretical computer science
Automated theorem proving
Logic in computer science