About the Book
This is a mathematics textbook with theorems and proofs. The choice of topics has been guided by the needs of computer science students. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and yet sufficiently elementary for undergraduates. In order to provide a balanced treatment of logic, tableaux are related to deductive proof systems. The book presents various logical systems and contains exercises. Still further, Prolog source code is available on an accompanying Web site. The author is an Associate Professor at the Department of Science Teaching, Weizmann Institute of Science.
Table of Contents:
Preface.- Introduction.- Propositional Calculus: Formulas, Models, Tableaux.- Propositional Calculus: Deductive Systems.- Propositional Calculus: Resolution and BDDs.- Predicate Calculus: Formulas, Models, Tableau.- Predicate Calculus: Deductive Systems.- Predicate Calculus: Resolution.- Logic Programming.- Programs: Semantics and Verification.- Programs: Formal Specification with Z.- Temporal Logic: Formulas, Models, Tableaux.- Temporal Logic: Deduction and Applications.- Appendix: Set Theory; Further Reading; Bibliography; Index of Symbols; Index.
Review :
From the reviews of the second edition: Mathematical Logic for Computer Science (Second Revised Edition) by Mordechai BenAri, Springer, 2001, paperback: ISBN 1852333197, 24.50 GBP/ $ 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 firstyear 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 "FirstOrder Logic and Automated Theorem Proving" by M. Fitting (second edition, SpringerVerlag, New York, 1996). The author shows a very careful build up, where the basic concepts and techniques are introduced first for propositional logic (chapters 24), then "lifted" to the predicate logic (chapters 57), and finally to temporal logic (chapters 1112). 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, operator is mentioned, but the arithmetic comparison operators are not. (A minor comment: the Prolog program 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, socalled 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. Krzysztof R. Apt "The text of the this second edition has been rewritten to a large extent. ... Some material has been added. The most essential additions are sections on binary decision diagrams, on constraint logic programming, and on the completeness of the Hoare logic. ... The book is well made as an introduction for computer scientists. It may even be a nice additional reading for mathematicians and logicians in undergraduate courses." (Siegfried Johannes Gottwald, Zentralblatt MATH, Vol. 1009, 2003) "This is a rewritten version of a book first published in 1993. It is intended for undergraduate computer science students, using an approach that the author promises as broad, elementary and rigorous. ... The book is broad, dealing with more subjects than is usual at undergraduate level, for example resolution and temporal logic. ... the writing is well structured, with precise definitions, propositions and theorems. Each chapter ends with exercises. ... In conclusion, this is an excellent book." (F. Aribaud, Computing Reviews, January, 2002) "The name of the book corresponds very much with its content. It is about mathematical logic and it is intended for computer scientists. ... The book is indeed broad: it covers both propositional and predicate logic ... . I would like to stress that the author uses a very nice didactic approach. ... The book is indeed elementary: no special preliminary knowledge is needed. The presentation is quite clear and illustrative. Even the most complex proofs ... are explained in the most constructive way possible." (Petr Cintula, Neural Network World, Vol. 12 (4), 2002) "The book is a serious contender to be the textbook of choice for the undergraduate students. ... All chapters are very carefully written. The concepts are clearly introduced with plenty of examples and helpful comments. ... This provides a useful context in which one can appreciate the properties and limitations of the introduced formalisms. ... 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." (Kryzstof R. Apt, Theory and Practice of Logic Programming, Vol. 2 (1), 2002)
