Wos explains the methodology and details of his experiments with the OTTER theorem-proving system. The common goal of these experiments was the quest for shorter proofs, but the reader is also given general hints and tips for using the various options that OTTER provides. The experiments stem from three domains. Complete listings of input files and the proofs found are provided in the book (occupying more than 180 pages). OTTER and the input files are included on a diskette so readers can use them for their own experiments (on PCs and Macs).

The notebook format leads to interesting in-depth analyses of the experiments, but there is some redundancy, and some key concepts are not abstracted. As can be expected from Wos, the book contains various challenges, notes on problems (with respect to the prover and the problem domains), and trends he expects for the future.

The book provides excellent insight into the use of  OTTER  and into the experimental work of a renowned researcher. In contrast to published papers, it also describes dead ends and the author’s struggle to leave them. This material encourages new researchers and provides insight into methods of overcoming such problems. Although I expected a strong bias in favor of OTTER, I believe that this bias is too strong: there is hardly any mention of other provers and techniques in the text or references (which reduces the potential readership). Even references to some techniques employed by OTTER (but stemming from work by other researchers) are missing. Also, I would have liked to see remarks on the transfer of experience with OTTER to higher levels, either to other theorem provers or to automated deduction in general.

I recommend the book to people who want to solve harder problems using OTTER and to those members of the deduction community who are interested in controlling the search of a theorem prover. The book is not intended as an introduction to automated theorem proving and cannot be used as a textbook.