Jean Goubault-Larrecq and Ian Mackie Proof Theory and Automated
Deduction Kluwer Academic Publishers Dordrecht/Boston/London, 1997
Pp. xv + 425 ISBN 0792345932 (Hardback) Price: $ 155 U.S., £ 96
Proof Theory and Automated Deduction certainly fills a niche in the market for text-books in mathematical logic. Although there are enough quality books on either Logic or Proof Theory, Automated Theorem Proving is somewhat lacking in the text-book department, especially one that covers such a wide range. There are other texts that cover some of this material in more detail-e.g. Melvin Fitting's First Order Logic and Automated Theorem Proving Springer-Verlag, 1996)-but most of the literature in this field is derivative from Ph.D. theses and not especially pedagogical in spirit. In contrast Proof Theory and Automated Deduction is clearly a compilation of lecture notes for an overview course at the intersection of both fields. There are, however, many details in this material that need to be filled in by the lecturer and the students.
The book begins with the classical propositional calculus, including all the usual groundwork for a 3rd year logic course: Hilbert Systems, Natural Deduction Gentzen systems and the associated theorems (soundness, completness deduction etc.) but also covers several non-standard calculi, intuitionistic, linear, modal and temporal logics. Overall, more than half the book is devoted to propositional systems. And a good thing too, since there is both a wide variety of propositional logics as well as significant range of theorem provers for them.
The authors quickly cover the main automated decision procedures (they call them "algorithms" but only in the most general sense--there is no software of any sort to be found in this book, something of a drawback for those inclined towards experimental computer science) for each of these proof systems, but not in enough detail to touch on active research in these areas.
Such broad coverage inevitably leads to a surficial treatment of some topics. For example, in the area of classical propositional theorem proving, there are a large number of variants to the methods known as "resolution" and "tableaux" that could have been introduced and discussed as propositional techniques. While these varients (e.g. clause ordering strategies for resolution) are quickly covered in chapters dealing with first-order systems, it would have better (pedagogically anyway) to discuss them as variants to propositional resolution. First order quantification and substitution rules should be treated as twists to propositional strategies rather than integral to them.
That this book need backup texts from both meta-logic and computer science is evidenced by the fact that it treats both Göedel's incompleteness theorem and Cook's theorem (that SATISFIABILITY is NP-complete) as "digressions". Of course, from the point of view of automated theorem proving, these topics should be background knowledge, but Cook's theorem especially can rightly be considered essential material to understanding the inherent limitations of any automated theorem proving procedure. Indeed, the implications of the still open question of whether P = NP is a siginificant motivation for exploring automated theorem proving techniques for the propositional calculus in the first place. This topic, in connection with automated theorem proving has been the subject of intensive research since the 1970's and by none other than Cook himself and yet there is little mention of the implications of complexity theory for automated reasoning. It is as if complexity needed to be mentioned merely for the sake of completeness.
There are other limitations to this book too. When comparing the various systems that they describe, for example, Bibel's "connection method" and tableaux methods, the authors make true statements about their relative merits (they are essentially equivalent), but miss an opportunity to demonstrate such equivalence. This kind of task could be given as an excercise to the student, for example.
From the point of view of computer science, those interested in formal methods will be gratified to see an entire chapter devoted to the Curry-Howard correspondance (between the typed lamda calculus and intuitionistic propositional calculus), but as with much of this book, background motivation and supporting documentation is required. Similarly, the techniques of term rewriting, sorted-logics and equational systems, while not strictly "automated deduction", cater to computer scientists. And while book on logic and computing wouldn't be complete without touching on logic programming, 15 pages is hardly enough to do anything other than mention constraint logic programming, and-parallelism and or-parallelism. As with the rest of the book, supporting material from the lecturer is required.
One measure of quality in a text-book is the usefulness of the excercises. Here, this book succeeds only in so far as the excercises are footnotes to the text, i.e. content that is given to the reader to work out. In the context of a course, the lecturer would have to construct her own set of problems.
All in all, the good news is that this volume fills a significant lacuna in the text-book literature, albeit at an excessive cost (how many students can afford $155 for a book these days?) The bad news is that it covers too much material in insufficient depth and cannot stand alone without lectures and supplementary material. My hope is that this volume will serve as an inspiration for others to develop similarly oriented but more complete texts that cover the same material.
Andre' Vellino. andre@ai.iit.nrc.ca