This page (and its dependents) is mirrored for your convenience.
Please conserve bandwidth by using the appropriate site from:
This page is still under construction, so it is by no means complete.
For better service to the Mechanized Reasoning community we will need
your help. Please contribute!.
Send links, material to fill in blanks, suggestions, encouragement, or
donations by clicking
To understand what automated reasoning is, we must first understand what
reasoning is. Reasoning is the process of drawing conclusions
from facts. For the reasoning to be sound, these conclusions must follow
inevitably from the facts from which they are drawn. In other words,
reasoning [...] is not concerned with some conclusion that has a
good chance of being true when the facts are true. Indeed, reasoning as
used here refers to logical reasoning, not of common-sense reasoning or
probabilistic reasoning. The only conclusions that are acceptable are those
that follow logically from the supplied facts.
The object of automated reasoning is to write computer programs
that assist in solving problems and in answering questions requiring
reasoning. The assistance provided by an automated reasoning program is
available in two different modes. You can use such a program in an
iterative fashion; that is, you can instruct it to draw some conclusions
and present them to you, and then, based on your analysis of the
conclusions, it can in the next run execute your new set of
instructions. Or you can use such a program in a batch mode; that is, you
can assign it an entire reasoning task and await the final result.
Larry Wos; Ross Overbeek; Ewing Lusk; Jim Boyle
Automated reasoning: Introduction and Applications.
McGraw Hill 1992.