Automated reasoning research aids in the development of computer programmes that enable computers to reason completely automatically. It is part of AI, but it also has ties to theoretical computer science and philosophy. Some attribute automated reasoning, or automated deduction, to the 1957 Cornell Summer Meeting, which brought together a large number of logicians and computer scientists. Others assert that it began earlier, with Newell, Shaw, and Simon's 1955 Logic Theorist programme or Martin Davis' 1954 implementation of Presburger's decision procedure (which proved that the sum of two even numbers is even).

Although automated reasoning is a significant and popular area of research, it experienced an "AI winter" in the 1980s and early 1990s. However, the field was later resurrected. For instance, Microsoft began utilising verification technology in 2005 and plans to include a logical specification and a checking language in their 2012 version of Visual C.

Why automated reasoning?

An automated reasoning system should be able to make logical inferences towards a goal given a set of assumptions. Automated reasoning computers can be used to automate and apply logical reasoning to tasks like proving theorems, verifying proofs, and designing circuits. Logic can also be used in automated reasoning in the form of analogy, induction, abduction, and non-monotonic reasoning. However, in mathematics and logic, the term "automated reasoning" is most commonly used to refer to deductive reasoning.

What is meant by problem domain?

The term "problem domain" refers to the set of problems that an automated reasoning programme is presented with. Problem assumptions, which are statements that provide relevant information to the automated reasoning system, and problem conclusions, which are the questions posed to the system, are examples of problem domains. The reasoning programme will take the problem domain as input and output a solution, such as the proof's accuracy. When a solution is found or resources are depleted, an automated reasoning programme will end.

Research Contributions 

Alfred North Whitehead and Bertrand Russell's Principia Mathematica was a seminal work in formal logic. The purpose of Principia Mathematica - also known as Principles of Mathematics - was to derive all or some of the mathematical expressions in terms of symbolic logic.

Logic Theorist (LT) was the first programme to "mimic human reasoning" in the proof of theorems, developed in 1956 by Allen Newell, Cliff Shaw, and Herbert A. Simon. It was demonstrated on fifty-two theorems from chapter two of Principia Mathematica, proving thirty-eight of them. In addition to proving the theorems, the programme discovered a more elegant proof for one of the theorems than Whitehead and Russell's.

Proof systems

Boyer-Moore Theorem Prover (NQTHM)

John McCarthy and Woody Bledsoe influenced the design of NQTHM. This was a fully automatic theorem prover built in Pure Lisp that began in 1971 in Edinburgh, Scotland.

The following were the main features of NQTHM:

• Lisp is used as a working logic.
• The use of a definition principle for total recursive functions.
• Rewriting and "symbolic evaluation" are frequently used.
• Based on the failure of symbolic evaluation, an induction heuristic was developed.

HOL Light 

HOL Light, which is written in OCaml, is intended to have a simple and clean logical foundation as well as an uncluttered implementation. It's essentially another proof assistant for higher-order logic in the classical sense.

Coq

Coq is a French-developed automated proof assistant that can extract executable programmes from specifications as either Objective CAML or Haskell source code. The Calculus of Inductive Constructions makes sure that properties, programs, and proofs are all written in the same language (CIC).

Uses

Deductive reasoning is the most common application of automated reasoning, which is used to find, check, and verify mathematical proofs using a computer system. Checking proofs with an automated reasoning system ensures that the user has not made any errors in their calculations. Moreover, automated reasoning can be used in a variety of fields, including mathematics, engineering, computer science, and non-mathematical applications such as answering philosophical questions. Many of these other subjects, on the other hand, must be represented in a language that the programme can understand.

AI and automated reasoning

Automated reasoning is considered a sub-field of AI. Both methods and implementations, however, are distinct enough to be considered separate entities. For example, AI frequently employs a type of logic known as modal logic, which combines classical logic with the expression of modality (possibilities or impossibilities). The term AI can also refer to a computer that acts like a human, which is in contrast to how automated reasoning works.

Conclusion

Automated reasoning is commonly used in theorem proving. However, theorem provers frequently require human guidance and thus qualify as proof assistants. In some cases, new approaches to proving theorems have emerged. A good example is the logic theorist. The programme came up with a proof for one of Principia Mathematica's theorems that was faster (fewer steps) than Whitehead and Russell's. Furthermore, a growing number of problems in formal logic, mathematics, and computer science are being solved by automated reasoning programmes. The TPTP (Sutcliffe and Suttner 1998) is a regularly updated library of such problems. It happens every year at the CADE conference, where automated theorem solvers compete against each other.

Image source: Unsplash