Automated reasoning

From Wikipedia, the free encyclopedia

Automated reasoning is an area of computer science dedicated to understanding different aspects of reasoning in a way that allows the creation of software which allows computers to reason completely or nearly completely automatically. As such, it is usually considered a subfield of artificial intelligence, but it also has strong connections to theoretical computer science and even philosophy.

The most developed subareas of automated reasoning probably are automated theorem proving (and the less automated but more pragmatic subfield of interactive theorem proving) and automated proof checking (viewed as guaranteed correct reasoning under fixed assumptions), but extensive work has also been done in reasoning by analogy, induction and abduction. Other important topics are reasoning under uncertainty and non-monotonic reasoning. An important part of the uncertainty field is that of argumentation, where further constraints of minimality and consistency are applied on top of the more standard automated deduction. John Pollock's Oscar system is an example of an automated argumentation system that is more specific than being just an automated theorem prover. Formal argumentation is subfield of artificial intelligence.

Tools and techniques include the classical logics and calculi from automated theorem proving, but also fuzzy logic, Bayesian inference, reasoning with maximal entropy and a large number of less formal ad-hoc techniques.