In the authors’ words, this book is intended for computer scientists interested in automated theorem proving in classical logic. It contains a thorough presentation of formal logic and many proof techniques. This treatment of methods for automated proving of theorems expressed in logic is carefully and clearly written. The mathematical background is presented precisely and elegantly. I wish all authors took such care in writing books. In discussing the content of the book, the authors’ final paragraph from the preface gives the scope:

So, a brief outline of the book is this. We begin with propositional logic, move on to first-order logic, then finish up with first-order logic with equality. For each of these we present both resolution and semantic tableau systems as primary. Implementations of semantic tableaux in Prolog are given, and similar implementations of resolution are outlined as projects. We also present natural deduction, Gentzen sequent calculi, and axiomatic systems, because these require little additional work and are common in the literature, though they are generally less appropriate for automated theorem proving. Also, for each level of logic that we consider we discuss necessary semantical background: Boolean valuations in the propositional case; models in the first-order case; and normal models in the first-order case with equality. Soundness and completeness of our theorem provers is established. Details of syntax as well as semantics are presented, including normal form theorems. In general, we use the device of uniform notation, due to R. M. Smullyan, which allows us to have many connectives and quantifiers present in our language without the need for elaborate theorem provers with many special cases. We hope to keep it clean and elegant.

The authors have succeeded admirably in giving a clean and elegant account of a technical topic. The examples of Prolog code are readable. The authors, by their own admission, have sacrificed efficiency for clarity. The subject matter, automated theorem proving, may be of limited interest, but for anyone interested in a very clear presentation of the theory underlying automated theorem proving--one biased toward computer scientists--this book is a must to read.