The authors start by providing a detailed description of the ML system for developing theorem proving programs. They then go on to the main topic of the book, the HOL theorem proving system, developed on top of ML. HOL is a reasoning system for higher-order logic. The bulk of the description is composed of the technical details for using the system (syntax rules, built-in operations and features, and so on) plus a few well-chosen extended examples. The last chapter offers a few suggestions by way of example on strategies and heuristics for theorem proving in the HOL environment, but this aspect of theorem proving is not meant to be a significant part of the book. The book is divided into five parts--a tutorial overview of how the system is used; a detailed description of the syntax, semantics, and operations of ML; a presentation of the syntax and semantics of a sequent form of higher-order logic; a description of the basic operations of the HOL top layer; and, finally, a description of theorem proving in HOL.
The stated purpose of the book is to present the HOL system so readers may become HOL users. It serves that purpose quite well. The level of detail is appropriate, and the examples are sufficient (although perhaps a bit sparse). The book clearly was not intended as a general introduction to automated reasoning or higher-order logic and should probably not be used as such. It would be difficult for readers not already familiar with most aspects of automated reasoning and higher-order logic to follow this book, but it must be stressed that the authors did not intend the book for such readers. The intended readers appear to be those who know about automated reasoning and want to learn to use this particular system. It is especially pleasing that the preface contains instructions for obtaining the HOL system software both on tape and by anonymous file transfer.
This book may not be useful as a primary text in a course on automated reasoning because it assumes the readers already know much of that material. It would certainly make an excellent lab manual for courses using the HOL system or even the ML system, however. No exercises are provided (probably because the book was not intended as a course text), but the demonstration of how to implement various reasoning systems within ML would be an added attraction in many courses on automated reasoning.
The physical presentation of the book seems adequate, as does the index. The authors provide few references (26 in all), but there does seem to be at least one reasonable reference for most of the important topics mentioned in the text.
The strong point of the presentation is the amount of detail and the care in describing how to do things within the ML and HOL environments. Few other reasoning systems are described in such detail. If the book has a weakness, it is the lack of small examples at strategic points. In many cases, especially in the second half of the book, several chapters of details are followed by a major example. I could follow the presentation quite well because of my own background, but I would sometimes have found it helpful to see some of the details illustrated. On the whole, however, for an experienced reader, this book is an excellent presentation of a sophisticated reasoning system.
