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
This page contains the following items:
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.
The field of mechanized reasoning is still oriented mostly towards
basic research. This research is carried out by
university research groups or
individual researchers, and
research groups in an industrial context.
Discussion of results and trends on mechanized reasoning takes places in the
international Conferences and
(for more specialized topics) on public
mailing lists by e-mail.
Link to appear -- contributions encouraged.
Until then, check out the extensive
Bibliography an automated deduction maintained by
A Belorussian translation of this page
can be found here.
This page comes to you courtesy of
Michael Kohlhase and
Last updated 2 September 1996.