Automated reasoning is an area of computer science and mathematical logic dedicated to understanding different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence it also has connections with theoretical computer science and even philosophy.
The most developed subareas of automated reasoning 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). 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.
Tools and techniques of automated reasoning include the classical logics and calculi, fuzzy logic, Bayesian inference, reasoning with maximal entropy and a large number of less formal ad-hoc techniques.
Read more about Automated Reasoning: Early Years, Significant Contributions, Proof Systems, Applications
Famous quotes containing the words automated and/or reasoning:
“Now, as always, the most automated appliance in a household is the mother.”
—Beverly Jones (b. 1927)
“Reasoning is the pastime of my whole household, and all this reasoning has driven out Reason.”
—Molière [Jean Baptiste Poquelin] (1622–1673)