zbMATH — the first resource for mathematics

Automated reasoning and the discovery of missing and elegant proofs. (English) Zbl 1058.68102
Princeton, NJ: Rinton Press (ISBN 1-58949-023-1/hbk). xv, 372 p. (2003).
This book provides a deep and exclusive view on research in the area of automated theorem proving. The presentation of the book and its material make it very different from the usual textbooks in this area. The authors have it very well understood to make their fascination of the area understandable to a reader.
The book discusses two different motivations for automated theorem proving. First, there is the search of a proof for an open, still unanswered mathematical conjecture. Second, there is the search for more elegant, shorter, or surprising proofs of existing theorems. Numerous examples are given throughout the book that illustrate both challenges. They are taken from various fields of mathematics such as group and lattice theory, Boolean algebra, modal and other logics.
The adventure of automated theorem proving is illustrated by focusing on the history and capabilities of the resolution-style theorem prover OTTER. The book introduces the theoretical and algorithmic foundations of OTTER and discusses in particular the strategies used by the theorem prover to find mathematical proofs. The book illustrates how OTTER approaches certain proof problems, how it is able to solve them and why it is capable to succeed. The role of OTTER as an automated reasoning assistant that interacts with a human and assists in exploring mathematical problems is given special attention.
A sequence of dialogues between fictitious researchers representing different opinions with respect to automated theorem proving concludes each chapter and provides an amusing summary on what has been presented so far and on what will follow in the next chapters. The book concludes by proposing two variants of the famous Turing test, which appear to be more appropriate in the context of automated theorem proving. Instead of imitating a mathematician’s way of proving a theorem, the authors propose to challenge theorem provers in the way they present automatically found proofs to humans. The theorem provers should be able to invent a notation and presentation that makes proofs easy to understand and to follow by a human. Furthermore, a theorem prover should be able to analyse its own progress and operate in a self-analytical mode, which allows it to abandon proof paths that seem to appear non-successful.
A CD including the theorem prover, a detailed documentation, and a comprehensive set of examples complement the book and allow the reader to experiment with the theorem prover OTTER.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
03B35 Mechanization of proofs and logical operations