Automated Reasoning:
Introduction and Applications
(2nd edition)
by
Larry Wos,
Ross Overbeek,
Rusty Lusk, and
Jim Boyle,
McGraw-Hill, 1992.
This book offers
a thorough introduction to the elements of automated reasoning.
Included are examples of the clause language used by the program
Otter,
and the inference rules and strategies that give automated
reasoning programs their power. Then, step by step, the book shows
how to harness this power to tackle complex challenges in abstract
mathematics and formal logic, logic circuit design, circuit
validation, and real-time systems control. Featured are successes in
answering challenging questions from a variety of fields. Numerous
open questions are also provided---questions that are of interest to
experts in the field, whose answers are unknown, and which can be
attacked with an automated reasoning program. In order to assist in
this attack, the book includes a diskette version of Otter 2.2 and a
tutorial for getting started in the use of this versatile and
extremely powerful automated reasoning program.
For further information, contact
Larry Wos ([email protected]).
Contents of the Book
- Introduction --- 1
- Learning Logic by Example --- 15
- Puzzles --- 53
- Alternative Representation and Equality --- 103
- Harder Puzzles --- 143
- Summary and Partial Formalization --- 187
- Logic Circuit Design --- 235
- Logic Circuit Validation --- 277
- Research in Mathematics --- 297
- Research in Formal Logic --- 345
- Real-time Systems Control --- 389
- Program Debugging and Verification --- 407
- Open Questions, Challenge Problems, and Research --- 467
- Prolog: Logic as a Programming Language --- 487
- The Formal Treatment of Automated Reasoning --- 513
- A Tutorial on the Use of OTTER --- 571
- The Art of Automated Reasoning --- 613
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.