The following* is a negative review by Professor Eric Martin of the first edition of this textbook. I see my books (and papers, too, for that matter) as work in progress, and thus am thankful for all feedback that might help me in this task. This I do, at a time when the Internet allows for a (Marxist) real-time flow of information, by posting online and regularly updating addenda and errata lists, and by eventually completing new editions with the additions and corrections as soon as it is feasible. While I thank Professor Eric Martin for his scrutiny, which I was not timely aware of for the completion of the second edition (published in January, 2020), I cannot but disagree with some of his criticism. In due time, I hope to be able to reply to all his concerns by commenting on his original text with this font in this color.

Computational logic. Volume 1: Classical deductive computing with classical logic. (English) Zbl 1408.68001

Texts in Computing 19. London: College Publications (ISBN 978-1-84890-280-0/pbk). xviii, 464 p. (2018).

Following an 11-page introduction, the book is divided into four parts. Apparently, there is nothing wrong with the introduction, though running at 11 pages, as it does, a lot of things could have gone wrong. {

\begin{itemize}
\item[–]Mathematical notions: Set-theoretic concepts. Boolean algebras. Lattices. Graphs and trees. Mathematical induction.
\item[–]Classical computing: Formal languages and grammars. Regular languages. Context-free languages. The pumping lemmas. Derivations and ambiguity. Recursively enumerable and recursive languages. The Chomsky hierarchy. Deterministic and indeterministic finite-state machines. Decision problems. Transducers, Moore and Mealy machines. Deterministic and indeterministic pushdown automata and acceptance criteria. $$LR(0)$$ and $$LR(1)$$ grammars. Deterministic and indeterministic Turing machines. Linear bounded automata. Turing-reducibility. The Halting problem. Space and time complexity classes. Polynomial-time reducibility, NP-completeness and NP-hardness.
\item[–]Classical deduction and classical logic: Propositional and first-order languages. Inference rules. Valuations and interpretations. Logical consequences, satisfiability. Completeness. Undecidability, decidability and complexity of first-order classes of languages. Substitution, unification. Equality. The Frege-Łukasiewicz axiom system. Natural deduction. The sequent calculus. Tarskian semantics. Herbrand semantics. Algebraic semantics.
\item[–]Classical deductive computing with classical logic: Proof of NP-completeness of the satisfiability problem. Normal forms (prenex, Skolem, NNF, CNF, DNF and special cases of the satisfiability problem. Herbrand’s theorem. Resolution for propositional logic and first-order logic. Hyperresolution. The Prover9-Mace4 theorem prover software. Paramodulation (equality in resolution). Analytic tableaux for propositional logic and first-order logic. Logic programs. SLD-resolution. Prolog. Negation as failure.
\end{itemize}

} So the monograph provides introductory material to three fields of study: automata theory, logic, and logic programming. Since there is a plethora of publications for all three, most readers will likely have at least two expectations: that the structure of the book ties those fields of study as closely as possible; and that what is standard, classic material be presented in a way that benefits from decades of experience and be of high pedagogical value. Unfortunately, readers will most probably, very quickly find out that the book fails on both accounts, that the formal presentation is of very low quality, and they might even become extremely frustrated and conclude that for any part of the material, there are many sources of information where a much better job has been done. Readers’ expectations should be objectively based, i.e. based on information provided in the book, namely on the back-cover synopsis. This, in the case of this book, reads as follows: “The objective of the main text is to provide the reader with a thorough elaboration on both classical computing and classical deduction with the classical first-order predicate calculus with a view to computational implementations. As a complement to the mathematical-based exposition of the topics we offer the reader a very large selection of exercises. This selection aims at not only practice of discussed material, but also creative approaches to problems, for both discussed and novel contents, as well as at research into further relevant topics.” Nowhere in this passage – nor elsewhere in the book, for that matter – is it claimed “that the structure of the book ties those fields of study as closely as possible” and/or “that what is standard, classic material [is] presented in a way that benefits from decades of experience and [is] of high pedagogical value.”

Besides the lack of structure and the slackness of presentation, the reader can legitimately wonder whether all those notions will eventually be used, and for those that will (as indeed not of all them will), where in the book that is, and whether this or that notion is promised to play an essential or a marginal role. The fact that the Index is minimal (e.g., “semigroup”, “monoid”, and even “algebra” are not part of the Index) seems to imply that readers have no other option but memorise them all, in their driest form, in case they turn out to eventually prove useful, as indeed the author does not always refer to where a notion is defined in case it is eventually used; when he does refer to a definition, it is often a nightmare to spot it, as definitions, theorems, examples, etc. are numbered independently and interfere. Professor Martin thinks the Index is minimal; I think it is proportionate. In particular, the mathematical notions of Chapter 1 are essentially omitted in the Index, as I guess the reader will autonomously self-refer to it in case of need. I also expect that anyone who can count to, say, 100, will be able to navigate easily in the numbered items in this book, even if, as sometimes is the case in other published texts, theorems and examples are numbered independently. But then, by posing an intellectual challenge of such a proportion as Professor Martin claims the numbering in this book does, I might have unwittingly given this book also the convenient property of staving off early onset dementia. The one more reason for you to peruse it.

Definitions are often imprecise, awkward, fuzzy, unclear. For instance, Definition 2.2.4 differentiates between a string that is “accepted” and a string that is “recognised”. Most readers would be hard pressed to understand the difference between both notions from the proposed definitions, and will be irritated at phrases of the form “if the final state qfQ is some accepting state qiA, 0≤in” rather than just “if the final state is accepting”, all the more so that a prior definition introduced the notation with a set A of accepting states, not a state of cardinality n+1 for some integer n that is in fact introduced earlier in Definition 2.2.4 to denote something totally different (the last index of a sequence of configurations). Even worse, the text is full of more or less serious mistakes. For instance, in Example 2.3.1, meant to demonstrate that the set of polynomials over x with an integral root is not decidable, we read “if some nZ it is the case that p=0”, which is formally very slack, to say the least, before having to remark that it is “obvious” that the specific algorithm that consists in, for a given polynomial p, enumerating values x and testing whether p(x)=0

, “will run forever”, and then conclude: “thus this set is in fact not computable”, thus being both grammatically and logically wrong\dots. These are just examples, randomly chosen as almost each and every page of the book could be used as an illustration of the poorness of presentation.

Generality is good, only if it proves useful, only if it is not gratuitous. For instance, what is the point in Definition 3.1.3 of writing “if ni

is an n-place operator and ϕ1, \dots, ϕn formulae, then i(ϕ1,…,ϕn) is a (compound) formula” when operators will then be nothing but negation and the usual binary Boolean operators (not to mention the useless introduction of the index i)? Useless generalisation is pushed much further, resulting in endless, contrived definitions. For instance, after the long Chapter 3 on logical form and logical meaning, where way too many definitions were introduced to awkwardly present the basic syntax and semantics of logical systems, Chapter 4 re-attacks with for instance Definition 4.2.1 to introduce “Tarski-style conditions for the classical consequence operation CnL for a (possibly empty) set ΓFL and any formula ϕ,ψFL”, such as “Cn(Γ,ϕψ)=Cn(Γ,ϕ,ψ)”, whereas in Chapter 3, means conjunction, but the fact that “classical” occurs in the title of Chapter 4 probably prompted the author to specialise what would be a potentially more general interpretation where would not mean conjunction (with as usual, messy notation, here, in particular and not exclusively, with the introduction of L as a subscript to Cn that is then immediately dropped). The lack of coherent structure strikes everywhere. For instance, after the long Chapters 3, 4 and 5 all dedicated to the syntax, semantics, and proof theory of propositional and first-order logic, the more specialised Chapter 6 on “Algebraic semantics: Boolean algebras” ends with two absolutely basic syntactic definitions: “An expression of the form ϕ(p1,…,pn) where the pi are propositional Boolean variables is called a propositional Boolean formula” and “An expression of the form 1x1…nxn(ϕ(x1,…,xn)) where the xi are individual Boolean variables and the i{,}

is called a quantified Boolean formula” (with expectedly, unnecessarily unfamiliar symbols, unnecessary indexes, unnecessary parentheses\dots); why here? why there at all?\dots

The book is full of exercises, of four kinds. First, straightforward exercises to test the understanding of basic notions, for instance, Exercise 3.1.2.3: “Identify the closed and the open FO formulae. For the open formulae, give their universal closure. 1. xyP(x,y)

\dots”. Second, exercises where the reader is asked to complete the proof of a result in the text, for instance Exercise 3.5.3.4: “Complete the proof of Theorem 3.5.8”. Third, exercises which are just classical results that the text left out, for instance Exercise 3.5.1.2: “Let Θ be an axiomatizable theory. Show that if Θ is complete then Θ

is decidable.” Fourth, very open-ended exercises, for instance Exercise 2.3.12: “Research into Post’s Correspondence Problem and give its main points”. While it is good to have many exercises, those proposed in the book do not have much originality and not much thought has been given to making sure they are as insightful and valuable as possible. As an instructor, when using a textbook I like to have a large selection of exercises from which to choose those that might better fit the students’ skills and capabilities. The range of these is pretty (impressively) wide, and at this introductory level, at which the main objective is that students grasp the basic concepts by both practicing and ruminating, I am not really concerned with originality; as an author, thought is given to making sure that the exercises might contribute to this objective.  Most results are given in the text without proof (that is, are given with a proof that refers to an exercise asking for the proof), while most remaining results are given incomplete proofs, with again one reference or more to exercises asking to complete this or that part of the proof. Many readers would probably prefer to have a more self-contained body, with carefully written, complete proofs that prepare them better to tackling exercises, but it is true that considering how poorly proofs or proof sketches are written, the current design might still be preferable\dots A more self-contained book is hardly possible, as the second edition already runs at over 330 pages and there are still contents I think should be covered (e.g., formal verification). Giving complete proofs of all the main statements, while significantly taking space from more important contents would not bring any benefits for, in my view, mostly two reasons: firstly, complete proofs, original or in a different guise, are to be found in just about any “standard” book in the field and no book, self-contained or not, stands alone; secondly, my objective is that students learn how to make their own proofs. With the latter aspect in mind, when giving a complete proof I try to be as concise as possible, and when giving a sketch of (or just an idea for) the proof I aim at omitting some aspects that would perhaps make the proof-writing too easy an exercise. To be sure, this might conduce to what can be seen as “poor writing,” especially if one’s pedagogical objectives are stifled by one’s authorial aspirations.

There is substantial general, “philosophical” discussion that is consistently confused, unclear, meandering, and not illuminating at all. This sounds pretty much like most “philosophical” discussions. In any case, maybe I should be flattered, given that, despite my training (also) in philosophy, I did not intentionally engage in any “philosophical” discussion in this book.  The claim that with logical languages we are “not interested in formalizing questions, orders, commands, interjections, or ejaculations” seems to be the only spurt of humour. It is my turn to be puzzled: This was a spurt of humor? Was humor expected in a book entitled “Computational logic”?

The typography is terrible. Arguably, the author should not be the only one to blame: this criticism would be alleviated or would disappear if publishers did not consider that their job does not go beyond accepting any Latex file without bothering to quickly browse how the pdf looks like and perform minimal edits. I really don’t know what the curt statement “The typography is terrible” is meant to convey, as no specification is given, but one of the many reasons that made me decide to publish with College Publications, London – to the extent that they accept my submissions, that is – is the low cost of the books, a feature that aims at making information accessible to all. Professional proofreaders and typesetters would significantly increase the prices of the books. This said, I can assure critics that no potential issue passes undetected before a book is eventually published by them.

A second volume on nonclassical logics is promised, but it would not be surprising that most readers who have tried to study the first volume will not consider learning from the second one.

Reviewer: Éric

Martin (Sydney)

MSC:

 68-01 Introductory exposition (textbooks, tutorial papers, etc.) from computer science 03B70 Logic in computer science 68N17 Logic programming 68Q05 Models of computation (Turing machines, etc.) (MSC2010) 68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.) 68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) 68Q42 Grammars and rewriting systems 68Q45 Formal languages and automata 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

models of computation; classical logic; semantics; proof systems; logic programming; Prolog