1. Introduction
Krzysztof R. Apt
Mathematical Logic for Computer Science (Second Revised Edition) by Mordechai Ben-Ari, Springer, 2001, paperback: ISBN 1-85233-319-7, 24.50 £/ $ 39.00, xiv + 304 pages.
The book is a major revision of the first edition in which new material has been included and several sections have been completely rewritten. This justifies a book review of this edition.
In the last couple of years a number of excellent textbooks on mathematical logic for computer science students have appeared. This book is a serious contender to be the textbook of choice for the undergraduate students.
The author states in the preface that this book is ``a mathematics textbook, just as a first-year calculus text is a mathematics textbook.'' This explains the view taken by the author. The style is rigorous yet informal. Proofs of many results are included, though proofs of more advanced results are omitted. Several concepts and methods are illustrated by Prolog programs, an idea originally adopted in the excellent textbook for graduate students ``First-Order Logic and Automated Theorem Proving'' by M. Fitting (second edition, Springer-Verlag, New York, 1996).
The book is divided into the following twelve sections and two appendices:
1. Introduction
2. Propositional Calculus: Formulas, Models, Tableaux
3. Propositional Calculus: Deductive Systems
4. Propositional Calculus: Resolution and BDDs
5. Predicate Calculus: Formulas, Models, Tableaux
6. Predicate Calculus: Deductive Systems
7. Predicate Calculus: Resolution
8. Logic Programming
9. Programs: Semantics and Verification
10. Programs: Formal Specification with Z
11. Temporal Logic: Formulas, Models, Tableaux
12. Temporal Logic: Deduction and Applications
Appendix A: Set Theory
Appendix B: Further Reading
This shows a very careful built up, where the basic concepts and techniques are introduced first for propositional logic (chapters 2-4), then ``lifted'' to the predicate logic (chapters 5-7), and finally to temporal logic (chapters 11-12). The remaining chapters are about uses of these concepts for programming by means of logic programming, program verification and program specification.
All chapters are very carefully written. The concepts are clearly introduced with plenty of examples and helpful comments. Advanced results are mentioned without proofs. This provides a useful context in which one can appreciate the properties and limitations of the introduced formalisms.
One potential problem in the use of this book is that the Prolog programs can be understood only after having studied chapter 8 on Logic Programming (and on Prolog), while several Prolog programs appear earlier in the text. So an optimal use of this book requires moving back and forth in the text. From this point of view chapter 8 is too brief on Prolog (just 5 pages). In fact, very few aspects of Prolog are explained there. For instance, the is operator is mentioned, but the arithmetic comparison operators are not. (A minor comment: the Prolog programming presented on page 184 is simply incorrect and not ``illegal''.)
The book in fact could profit from an appendix which would concentrate on the basics of Prolog programming. At the present moment the reader cannot easily follow the presented programs, since not all concepts are properly explained. For example, so-called anonymous variables are used already on page 38 but never explained. The logic programmers may find it of interest that the chapter on logic programming includes also sections on concurrent and on constraint logic programming.
Another, possibly debatable issue, is the omission of the use of logic in Database Systems and Artificial Intelligence. From this point of view several types of logics, models and deductive systems are missing. In fact, the reader will find no references to relational algebra, constraint satisfaction problems, integrity constraints, nonmonotonic reasoning, modelling of beliefs, and no information about logic of actions, logic of causation etc.
One can argue that most of these uses of logic are too specialized for a textbook aimed at undergraduate students who will also take general courses on Artificial Intelligence and Database systems. On the other hand these uses of logic seem as relevant as those on which this book focuses: for program verification and specification.
Finally, the author chose not to include any chapter on the lambda calculus and the functional programming style, perhaps because this would lead to a discussion of higher-order programming. However, in several computer science curricula a functional programming language is actually taught before Prolog.
Perhaps a third edition of this book could be envisaged with additional chapters on these issues. This might make the book too comprehensive as a textbook but would provide an almost complete overview of the subject for the undergraduate students. Putting these minor shortcomings aside, this is an excellent textbook that can be heartily recommended to those who plan to teach an undergraduate course on mathematical logic within the computer science curriculum.