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

## Chapters

- A Sterling Pursuit
- Scott's Challenge
- Provocative Obstacles and the Means for Quashing Them
- The Methodology by Example
- Lukasiewicz's Challenge
- Group Theory
- Robbins Algebra
- A Biased Guide for Choosing OTTER Options
- Seeking Proofs Satisfying a Given Property
- Proof Checking
- Experimental Potpourri
- Research Topics
- Additional Useful Notes
- A Demanding and Noble Endeavor
- Appendix A: Featuring Various Strategies
- Appendix B: Example 1 Files and Proofs and

Input File for Cursory Proof Checking
- Appendix C: Example 2 Files and Proofs and

Files for Rigorous Proof Checking
- Bibliography
- Index

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

Larry Wos

wos@mcs.anl.gov