Automated reasoning is the area of computer science that is concerned with applying
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.
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 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.
Automated reasoning and AI
Automated reasoning 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 automated reasoning operates.