Two very elaborate theorem-proving programs called HERBY and THEO are the focus of this book. Both are included on an accompanying CD-ROM. They are written in clear ANSI C, and are very well documented. Their structures are analyzed in chapter 11 (HERBY) and 12 (THEO) They run under Unix: the CD-ROM includes an IBM compiler for AIX, the IBM version of Unix. This is not useful for everyone, but in any case, the programs are too large to run on machines for the general public.
Chapter 1 gives concise instructions for creating the executable versions of the programs. Chapters 2 and 3 are devoted to the preprocessing of the well-formed formulas of first-order predicate calculus: how to form keyboard expressions that are written in symbolic language, and how to use the program COMPILE to transform the well-formed formulas into clauses.
Chapter 4 presents the fundamental methods in automated theorem proving, in particular the processes of substitution and unification. As the book does not focus on the theory of automated theorem proving, the presentation is informal, and is based on examples.
Chapter 5 brings us to the heart of the matter. Herbrand's theorem on unsatisfiable sets of clauses is rewritten in terms of trees: to prove a theorem one has to build such a tree ending in Null clauses. But these semantic trees grow rapidly out of control. The program HERBY includes many heuristics that allow it to limit such growth: they are explained in chapter 7. And chapter 8 shows how to use HERBY.
In chapter 6, and its continuations (chapters 9 and 10), THEO, a much more sophisticated approach, is introduced. The semantic trees are refined in resolution-refutation proofs. Such proofs can be illustrated by a graph. Linear proofs, in which there is a single path of resolvents in that graph, are of special interest. In chapter 6, it is proved that every theorem has a linear proof, and more specific features of linear proof are scrutinized. Chapter 9 is a key chapter: there the author makes the most of his great experience in chess programs. THEO attempts to find a linear proof by carrying out an iteratively deepening depth-first search (starting from the observation that short clauses are more likely than long ones to yield a contradiction). Technically, THEO uses a large hash table to store information about clauses generated during the search. How to build this table and to use it in deriving the wanted proof are the concerns of chapter 9. THEO is a complex program, allowing several options, which are explained in chapter 10. Of course, each chapter ends with exercises (with some answers given in Appendix A).
This book and the accompanying CD summarize a long line of research on automated theorem proving. It is not an easy book, and sometimes the non-specialist may get lost; but with the detailed programs, the reader has access to an exceptional treatment of the matter.
