It is possible to read this book at various levels. It can form a good introduction to the resolution method of theorem proving, both from the theoretical and the practical point of view, for people new to symbolic logic and for logicians interested in computer logic. It is also a good starting point for beginning researchers who would like to follow the activities at the Argonne National Laboratories. At every level, enough cogent exercises and answers are supplied.
For those readers who have seen and liked the first edition of this book [1], my first, unfortunate message is that you need to purchase this second edition if you wish to stay in touch with, be active in, or teach computer logic from the point of view of the authors. First, it provides an easy way to learn to use OTTER, the prover that the authors are now using--the original interactive theorem prover (ITP) still exists, but is probably no longer supported. Unlike the ITP, OTTER is not an interactive system and so is not as easy to learn by doing. Second, the book contains many important additions.
The theorem-proving software developed at the Argonne National Laboratory is no longer the only such software available in the public domain, as it was when the first edition of this book was published. The provers developed at Cornell by Constable and at the University of Texas at Austin by Boyer and Moore are also available. The newcomer to the field who is trying to get to know all three (at least superficially) will find this book of value in getting to know and understand the Argonne system as well as the research thrust at Argonne. For this purpose, the companion volume [2] is also useful.
After the preamble in chapter 1 (addressed to the complete newcomer), chapter 2 introduces the reader informally to the techniques of symbolic logic, starting with the elements of the language and going all the way to the concept of proof. Chapter 3 then introduces some logical puzzles, which are carefully formalized into a logical theory. The authors then indicate how the search for the solution to the puzzle can easily be looked upon as a search for the proof of a theorem. The chapter ends with a complete input file for OTTER, with a discussion (at this stage, necessarily somewhat cursory in places) of the part played by the various initial commands. The next chapter starts the real technical discussion on the proper use of the different resolution and modulation heuristics available in OTTER. It continues to use puzzles (albeit harder ones) as the vehicle of discussion. All of this material is based on the informal grounds established in chapter 2, but by the end of chapter 5, the student’s intuition about logic is fairly well developed. All these chapters contain detailed OTTER files--a major addition to the previous edition. The discussion of the weighing puzzle (billiard ball puzzle) in chapter 5 has been enhanced considerably.
The formalization of symbolic logic is brought closer to completion in chapter 6, in preparation for the detailed theoretical discussion of resolution and modulation techniques in chapter 15, which formed the basis of my understanding in the first edition. Chapter 6 is extended considerably over the previous edition. Section 6.11 contains a detailed introduction to the relation between OTTER and ITP, but not so detailed as to serve as a user’s guide. For that, the reader has to open the files on the PC disk that comes with the book or get a user’s manual from Argonne. The authors will also supply a Macintosh version of OTTER on request, although the non-executable files on that disk still have to be read with MS-DOS.
Chapters 7 and 8 illustrate the use of resolution in general and OTTER in particular for logic circuit design and validation. These chapters are not too different from the previous edition. The real extensions have occurred in chapters 9 and 10, which describe the research at Argonne on the use of automated theorem proving to aid research in mathematics and logic.
Chapters 11 and 12, on “Real Time Systems Control” and “Program Debugging and Verification,” have remained about the same as in the previous edition (I can sympathize with the fact that these torches were not picked up by younger members of the team). Chapter 12 discusses programming applications from the verification point of view as well as from the symbolic execution and abstract programming points of view. It is considerably longer than chapter 11.
Chapter 13 is entirely new. It replaces the discussion of expert systems in the previous edition with “Open Questions, Challenge Problems and Research.” It discusses the research of the authors and their colleagues in the areas of Robbins algebra, combinatory logic, and other logics such as equivalential calculus and many-valued sentential calculus. I was surprised to find that, while the authors discuss the relationship of their system with Prolog carefully in chapter13, they spend no time on the relationship between equivalential logic and the well-developed area of term rewriting systems.
Chapter 16 is a tutorial on the use of OTTER--not a user’s manual but a guide to intelligent use of the system. I feel somewhat sheepish in admitting that I should have studied this chapter carefully before starting to mess with the system. I probably could have saved myself a lot of grief.
