These web pages are a supplement to a book published by Academic Press in 1996.
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.
For further information, contact ([email protected]).