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 (wos@mcs.anl.gov).

Contents of the Book

  1. Introduction --- 1
  2. Learning Logic by Example --- 15
  3. Puzzles --- 53
  4. Alternative Representation and Equality --- 103
  5. Harder Puzzles --- 143
  6. Summary and Partial Formalization --- 187
  7. Logic Circuit Design --- 235
  8. Logic Circuit Validation --- 277
  9. Research in Mathematics --- 297
  10. Research in Formal Logic --- 345
  11. Real-time Systems Control --- 389
  12. Program Debugging and Verification --- 407
  13. Open Questions, Challenge Problems, and Research --- 467
  14. Prolog: Logic as a Programming Language --- 487
  15. The Formal Treatment of Automated Reasoning --- 513
  16. A Tutorial on the Use of OTTER --- 571
  17. The Art of Automated Reasoning --- 613

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.