Fundamentals of logic and computation. With practical automated reasoning and verification (Q2240968)

The volume is devoted to teach the fundamentals of logic and computation to undergraduates and higher-degree research students in computer science. The text is divided into three parts: \begin{itemize} \item The first part, \emph{Logic}, deals with classical propositional logic and first-order classical logic, and provides a short and informal introduction to intuitionistic, linear, and linear temporal logics. \item The \emph{Computation} part describes finite-state automata, regular languages, and pushdown automata, then moves to Turing machines, briefly sketching Kleene's recursive functions and the \(\lambda\)-calculus. It concludes with an overview of the basics of computability and computational complexity. \item The last part, \emph{Logic and Computation}, illustrates the Curry-Howard isomorphism. \end{itemize} Many exercises in the book require the student to formalise and prove statements in the Isabelle proof assistant or in the PAT model checker. From the point of view of a teacher who wants to deliver a course in logic and computation, the book has both nice aspects and drawbacks, depending on the specific program to teach and personal taste. The part on classical propositional logic introduces the axiomatic presentation of Boolean algebras instead of the algebraic definition as a bounded, complemented, and distributive lattice. For this reason, proofs of the soundness and completeness results, together with the construction of a classifying model, are absent in the book, which is a serious drawback in my humble opinion. On the other hand, I appreciate in Chapter~1 the presentation of both the natural deduction system and the sequent calculus with many examples fully worked out. The part on first-order classical logic is well written and useful in order to understand how to prove theorems inside the natural deduction calculus and also in the sequent presentation. I also found the presentation of the cut-elimination theorem quite clear. But I definitely found the lack of basic results in model theory unsatisfactory, like the compactness theorem and its applications. As before, the completeness theorem is stated but not proved: only a relative proof for the sequent calculus is shown, assuming that Hilbert's presentation is sound and complete. Chapter~3 aims at introducing intuitionistic, linear, and linear temporal logics. I particularly disagree with the presentation of the intuitionistic part: it is said that intuitionistic logic is less expressive than the classical system, which is simply false. In fact, the Gödel-Gentzen translation shows that intuitionistic logic is actually more expressive, by making distinctions which are invisible in the classical system, and these differences matter when studying computation. Moreover, the presentation of linear and linear temporal logics seems to be disconnected from the rest of the book. However, Section~3.4 presents model checking in a very neat and clear way. In general, I think that confining the use of the Isabelle proof assistant to exercises is quite demanding for the student, and a concise introduction to this system would have been welcome. The second part of the book starts with Chapter~4, illustrating automata theory. While the chapter is very well written, its connection with the logical side of the book is left unexplored. Chapter~5 is devoted to present Turing machines, Kleene's recursive functions, and the \(\lambda\)-calculus, with the two final sections illustrating the fundamentals of computability and computational complexity, respectively. Some historical notes are inaccurate, and the link between the stated but unproved Gödel's incompleteness theorems and the existence of non-computable functions is not explained. In general, the sections on computability and computational complexity are more a gallery of results, mostly without proofs, rather than a short but systematic presentation. In the second part of the book, many exercises require to use the PAT model checker but, as before, this system is not illustrated in the text, which, in my humble opinion, is troublesome for students. Finally, I found the third part of the book disappointing. It is just 8 pages long. It aims at illustrating the Curry-Howard isomorphism, which is sketched in the general case of intuitionistic propositional logic, but really developed just on the implicational fragment, and then provides a worked out example. It concludes mentioning that a similar correspondence between type theories and logics exists in other cases. I think that a textbook whose declared aim is to illustrate the interaction between logic and computation should leave more space and should go more into depth in this important and fascinating subject. Therefore, despite some good sections, I think the book fails to match the promises in its introduction, and the overall goal of providing a text to help teaching logic and computation as a unified subject has not been achieved.