The field of mathematical logic started in the 20th century, due in part to the efforts of mathematicians and others to understand the foundations and limits of mathematics. But today, one of the reasons for its study is certainly to aid in formalizing reasoning in a way that allows it (or some parts of it) to be carried out by machines. Such automated reasoning is, of course, unlikely to put human reasoners out of business any time soon (science fiction and other fantastic prognostications aside), but rather has the promise of, among other things, enabling automated theorem proving for formal verification of hardware and software systems. Therefore, it relates not only to classic areas such as mathematics, philosophy, and computer science (CS), but also to newer ones, such as systems theory and software testing.

Thus, it is clear that mathematical logic in general and automated reasoning techniques and technologies in particular have the potential to be of much interest to a great number of people, both theoreticians and practitioners. However, there is still a dearth of skilled workers and, in spite of improvements in recent years, even a lack of sufficient tutorial and expository material to bring newcomers into the fold. Part of the difficulty in this regard may be that treatises on the subject done in the classic style often focus, to a large extent, on mathematical rigor and finesse, which are quite laudable goals in their own right but tend to make life a little difficult for new learners, especially practitioners.

This book takes its place among those dealing with its subject in precisely such a setting. Like other Cambridge University Press books, it is written, edited, and produced well. Although some readers may justifiably gripe about their favorite topics being left out--as is sure to happen with any book--it is sure to fill a need for a well-rounded work that can serve both as a reference on a range of topics and as an introductory text, especially for those who wish to study the subject for its possible practical uses.

The book consists of seven chapters and three appendices. The first chapter introduces the basics of symbolic logic and related concepts such as Boolean algebra, syntax, and semantics. It gives a good historical perspective for many of the topics. The use of the objective Caml (OCaml) language is also introduced (the language itself is briefly summarized in Appendix 2). The second chapter introduces propositional logic and its concepts, such as tautology, validity, satisfiability, and the normal forms. The third chapter, arguably the best in the book, deals with first-order logic, discussing topics such as Skolemization, Herbrand’s theorem, unification, and resolution. The fourth chapter deals with equality; it features, among other things, a good discussion on rewriting and a concise treatment of Knuth-Bendix completion that is among the best I have seen. The fifth chapter deals with decidable problems and requires knowledge of (or willingness to learn) some graduate-level algebra, for the treatment of problems involving rings, word problems, and Gröbner bases. The sixth chapter is relatively short and deals with interactive theorem proving. The final chapter, “Limitations,” gives a brief perspective of Hilbert’s program, Gödel’s incompleteness theorem, and the general problems of undefinability and undecidability (with references to Tarski and Church). The three appendices give some of the necessary mathematical background, a primer on OCaml, and a discussion of parsing and printing of mathematical expressions, respectively.

Good features of the book are its overall readability, the good historical perspective conveyed while retaining its serious scholarly gravitas, and the use of OCaml to work with the concepts, presented alongside. Instructors will appreciate the detailed exercises given at the end of each chapter.