GC: n

CT: Reasoning is the ability to make inferences, and automated reasoning is concerned with the building of computing systems that automate this process. Although the overall goal is to mechanize different forms of reasoning, the term has largely been identified with valid deductive reasoning as practiced in mathematics and formal logic. In this respect, automated reasoning is akin to mechanical theorem proving. Building an automated reasoning program means providing an algorithmic description to a formal calculus so that it can be implemented on a computer to prove theorems of the calculus in an efficient manner. Important aspects of this exercise involve defining the class of problems the program will be required to solve, deciding what language will be used by the program to represent the information given to it as well as new information inferred by the program, specifying the mechanism that the program will use to conduct deductive inferences, and figuring out how to perform all these computations efficiently. While basic research work continues in order to provide the necessary theoretical framework, the field has reached a point where automated reasoning programs are being used by researchers to attack open questions in mathematics and logic, and to solve problems in engineering.

S: http://plato.stanford.edu/entries/reasoning-automated/ (last access: 2 March 2015)

N: 1. Automated reasoning is the science of
establishing methods that allow to replace human step-wise reasoning by procedures that perform individual reasoning steps mechanically and are able to find, automatically, suitable sequences of reasoning steps for deriving new knowledge from given one.
2. The object of automated reasoning is to write computer programs that assist in solving problems and in answering questions requiring reasoning.

S: 1. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.153.2873&rep=rep1&type=pdf (2 March 2015). 2. TERMIUMPLUS.

SYN:
S:

CR: artificial intelligence, computer science, semantic web.