The Automation of Reasoning: An Experimenter's Notebook with OTTER Tutorial

Larry Wos

These web pages are a supplement to a book published by Academic Press in 1996.


Abstract

This book, written in the style of an experimenter's notebook, presents results (both successes and failures) from numerous experiments with the automated reasoning program OTTER. Key to many of the experiments is the use of a new strategy, called the resonance strategy. The resonance strategy provides the basis for a methodology formulated for searching for elegant proofs with the aid of an automated reasoning program. While the focus here is on mathematics and logic, the successful search for shorter proofs can have application in other fields such as circuit design. Included are new proofs of problems in mathematics and in logic, numerous and varied challenges for possible research, comments to explain the nature of various experiments, and input and output files. This book also includes a diskette with the latest version of OTTER, including the source code in C, a users manual, test problems, input files, a load module for use on IBM-compatible personal computers, and a module for use on Macintoshes.

Input files and proofs

Chapters

  1. A Sterling Pursuit
  2. Scott's Challenge
  3. Provocative Obstacles and the Means for Quashing Them
  4. The Methodology by Example
  5. Lukasiewicz's Challenge
  6. Group Theory
  7. Robbins Algebra
  8. A Biased Guide for Choosing OTTER Options
  9. Seeking Proofs Satisfying a Given Property
  10. Proof Checking
  11. Experimental Potpourri
  12. Research Topics
  13. Additional Useful Notes
  14. A Demanding and Noble Endeavor
  15. Appendix A: Featuring Various Strategies
  16. Appendix B: Example 1 Files and Proofs and
    Input File for Cursory Proof Checking
  17. Appendix C: Example 2 Files and Proofs and
    Files for Rigorous Proof Checking
  18. Bibliography
  19. Index

For further information, contact (wos@mcs.anl.gov).


Larry Wos
wos@mcs.anl.gov