Mechanized Reasoning

This page (and its dependents) is mirrored for your convenience. Please conserve bandwidth by using the appropriate site from: USA, Germany.

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 here.

This page contains the following items:

What is Automated Reasoning

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.


Existing systems, related fields/pages, archives ...


Research groups and projects.

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 forums.

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.

Journals.


Organizations.


An annotated reading list.

Link to appear -- contributions encouraged.

Until then, check out the extensive Bibliography an automated deduction maintained by ORA Canada
A Belorussian translation of this page can be found here.

This page comes to you courtesy of Michael Kohlhase and Carolyn Talcott.

Last updated 2 September 1996.