For questions about Automated Reasoning concepts and research topics. Automated Reasoning is a sub-field of Artificial Intelligence concerned with the development of computer programs which can reason completely, or nearly completely, automatically.

Automated Reasoning (AR) is a sub-field of Artificial Intelligence concerned with the development of computer programs which can reason completely, or nearly completely, automatically.

Example of applications are automated theorem proving, proof checking, logic programming, circuit design and reasoning under uncertainity.

Tools used in AR include formal logic, fuzzy logic, bayesian inference and other formal ad-hoc techniques.

One of the first example of successful AR is Logic Theorist (LT), a computer program developed in 1956 by Allen Newell, Cliff Shaw and Herbert A. Simon, which eventually proven 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some. It is called "the first artificial intelligence program".