Automated reasoning (AR) was investigated by early researchers who developed algorithms that imitated step-by-step reasoning that humans use when they solve puzzles or make logical deductions. By the late 1980s and 1990s, AI research had developed methods for dealing with uncertain or incomplete information, employing concepts from probability and economics.
Many of these algorithms proved to be insufficient for solving large reasoning problems because they experienced a “combinatorial explosion”: they became exponentially slower as the problems grew larger. Even humans rarely use the step-by-step deduction that early AI research could model. They solve most of their problems using fast, intuitive judgments.
AR is the area of computer science that is concerned with applying reasoning in the form of logic to computing systems. If given a set of assumptions and a goal, an automated reasoning system should be able to make logical inferences towards that goal automatically. Computers that use automated reasoning can be used to automate and apply logical reasoning to activities such as proving theorems, checking proofs or designing circuits. AR can also use logic in the form of reasoning through analogy, induction, abduction and non-monotonic reasoning. However, the term automated reasoning is mostly used when referring to deductive reasoning in mathematics and logic.
The term “problem domain” is used to describe the class of problems presented to an automated reasoning program. Problem domains include problem assumptions, which are statements that provide relevant information to the automated reasoning system, and problem conclusions, which are the questions being asked of the system. The reasoning program will receive the problem domain as input and provide a solution as output, such as the accuracy of a proof. An AR program will terminate when a solution is found or resources are depleted.
The most common use of AR programs, to prove theorems, is accomplished through providing algorithmic descriptions to the calculus being used. Users are also required to define the class of problems the AR program will need to solve, the language the program will use to represent given information and what the program will use to implement deductive inferences.
The term automated deduction can also be used to refer to automated reasoning; however, automated deduction is used more narrowly in reference to using deduction logic in mathematics.
AR is mostly used with deductive reasoning to find, check and verify mathematical proofs using a computing system. Using an automated reasoning system to check proofs ensures that the user has not made a mistake in their calculations. Automated reasoning can also be used for applications in mathematics, engineering, computer science or non-mathematical purposes such as asking questions in exact philosophy. However, many of these other subjects still must be represented using a language the program can understand.
AR is considered to be a sub-field of artificial intelligence (AI). However, the methods and implementation of both are unique enough that they can be thought of as separate entities. For example, AI typically uses a type logic called modal logic, which uses classical logic while also expressing modality (possibilities or impossibilities). The phrase AI also has connotations denoting a computer which works like a person, which opposes how AR operates.
Automated reasoning is a fascinating field that helps to understand the real nature of mathematical creativity. Or more practically, to check the correctness of proofs in mathematics, supplementing or even replacing the existing ‘social process’ of peer review etc. with a more objective criterion. Also, to extend rigorous proof from pure mathematics to the verification of computer systems (programs, hardware systems, protocols etc.), supplementing or replacing the usual testing process.
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. 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 can use mathematical based logic to reason about the correctness, availability, security, and compliance of infrastructure and services. Providing a provable security initiative referring to a collection of automated reasoning tools for customers and developers to help provide higher security assurance.