automated reasoning

What is automated reasoning?

Automated reasoning is the area of computer science 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 toward 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. Automated reasoning can also use logic in the form of reasoning through analogy, induction, abduction and nonmonotonic 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 automated reasoning program will terminate when a solution is found or resources are depleted.

The most common use of automated reasoning 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 automated reasoning 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.

Uses

Automated reasoning 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 nonmathematical purposes. However, many of these other subjects still must be represented using a language the program can understand.

Automated reasoning and AI

Automated reasoning is considered to be a subfield 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 of 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, opposing how automated reasoning operates.