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 ([email protected]).

Larry Wos
[email protected]