The aim of this book is to serve both as an introduction to automated theorem proving (ATP) in first-order logic, and as a guide to current work on particular aspects of ATP. The intention is to give full details of the principles involved, whilst keeping the non-specialist in mind.…

There are two main themes in the book. The first concerns general techniques for performing proofs automatically, whilst the second concerns particular implemented systems to apply these techniques for specific purposes. With regard to the first theme the major approaches--natural deduction, sequentzen [sequent-calculi], resolution and the connection calculi--are discussed in detail.…Throughout this discussion an attempt is made to bring out the underlying relationships between these diverse approaches to proof. With regard to the second, three systems are described: Prolog, the Knuth-Bendix completion procedure and the Boyer-Moore theorem prover.…Prolog is related both to resolution and (cut-free) sequent calculi, whilst the distinct approaches to proof by induction applied by the Knuth-Bendix procedure and the Boyer-Moore system are shown to have fundamental connections.

--From the Preface

The author meets the aims set out in his preface. The brief introduction to first-order formal systems is sufficient to give the knowledgeable reader an idea of the notation used, while references to other texts serve to assist novices. The author’s practicality is characteristic of the text as a whole; he compares different forms of logical systems for their efficiency and ease of use. It is also instructive for the reader to see three ostensibly different systems compared and to have their similarities pointed out. The bibliography is up to date and comprehensive, and a number of illustrative exercises (some of which have solutions outlined) add to its usefulness. Perhaps all that is lacking is some discussion of material on computer-assisted proof as distinct from the automatically generated proof that is provided by the various logic for continuous functionals (LCF) systems, for instance. This area has wider applicability (and possibly wider utility) than ATP, and it would have been interesting to see the author’s views on this issue. Nonetheless, the book serves a useful purpose in combining a number of different systems in a single clear and unified exposition.