Browse Books

Reviewer: Alexei P. Stolboushkin

It is becoming increasingly clear that mathematical logic should be introduced at an early stage of the undergraduate computer science curriculum. This book is intended as a textbook for the first undergraduate course in mathematical logic for computer science students. The author starts by expressing his concern that the standard course in mathematical logic, intended for mathematics students, may not be suitable for computer science students, especially in their early years. For instance, for first-order logic, it seems appropriate for undergraduates in computer science to restrict their attention to countable structures. On the other hand, some topics that are not central in mathematical logic, such as proof methods and resolution, may deserve detailed consideration because of their wide application in computer science. The book has seven chapters: Introduction Propositional Calculus Predicate Calculus Resolution and Logic Programming Temporal Logic Formalization of Programs Further Reading Throughout the book, the exposition is elementary and mostly clear. Semantic tableaux, Gentzen systems, Hilbert systems, and resolution are introduced at the stage of propositional calculus. The discussion of predicate calculus does not go much beyond completeness. Logic programming is first discussed at an abstract level, with Prolog then briefly discussed as an example. The chapter on temporal logic introduces axioms for linear propositional temporal logic and proves their soundness and completeness. The last chapter gives an axiomatization for partial correctness of while programs (Hoare logic), with no proof of completeness, and then briefly discusses specifications with Z. Some incidental issues, such as decidability and complexity, are mentioned briefly. The numerous carefully chosen examples are helpful, especially when formal proofs are omitted. Nevertheless, I have the impression that the exercises could have been formulated better. Because of the pioneering nature of the book, it is natural that the presentation is not uniformly smooth. For instance, the discussion of Boolean operators is misleading. The operators are discussed by analogy with arithmetic operators, and the author suggests that the choice of a particular set of operators is motivated by psychological factors, such as whether they are interesting. The result concerning complete bases for Boolean operators is not even mentioned. The wording is careless at times, especially in informal discussions. For instance, mathematical logic is obscurely defined as “the study of Boolean expressions” (p. 3); statements in English are occasionally called “logical formulas” (p. 7 ); and Ben-Ari claims that “certain variants of resolution have proven to be” very efficient compared with other methods, although it is well known that resolution can be less efficient than exhaustive search. My main reservation about the book deals with what is not included. Traditionally, mathematical logic has three main branches: proof theory, model theory, and recursion theory. Of these, only one, proof theory, is presented in the book. This choice is not (and hardly could be) justified by applications in computer science. Without belaboring the point, we may just refer to the list of topics covered by the annual IEEE Symposium on Logic in Computer Science to see that abstract data types, database theory, and computational complexity, to name only a few, are areas of computer science where mathematical logic (and mostly not proof theory) is extensively used. The book represents a good, professional attempt to provide an undergraduate textbook on mathematical logic for computer science students, but it does not entirely fulfill its title and purpose, because of its omissions.