Errata to Nerode and Shore: Logic for Applications (1. Edition)

page 29, Exercise 4: missing right parenthesis in a and in b
page 104, Definition 6.7, item (2): "j+1st occurrence" should be "i+1st occurrence"
page 115, inference rule Generalization: should be: From \alpha infer \forall x\alpha.
page 145, Theorem 1.2: ``linear input resolution'' most likely should be in the statement of the theorem instead of ``linear resolution''
page 298, Exercise: The vowels in the medieval mnemonics of Aristotle's syllogisms (Barbara, Celarent, ...) do not uniquely determine the syllogism. E.g. Celarent and Cesare are both eae but they mean respectively AeB, BaC; AeC and BeA, BaC; AeC (here AaB means that all B are A, and AeB means that all B are non-A.) Celarent and Cesare belong to different patterns. It is not possible to solve the exercise using the book alone, as the patterns are not discussed.

Jussi Rintanen

page 32, the first line: either V(\alpha) = T and V(\beta) = T or V(\alpha) = F and V(\beta) = F
page 44, the last paragraph, line 5: A_1 :- or (A_1 <- )
page 65, the proof of Lemma 10.13: ... the length of the LD-resolution refutation ...
page 126, the last equation in the proof of Prop. 11.6: =v(\psi(\theta\sigma))
page 128, the first paragraph of Section 12, line 16: Thus the composition {x/h(y)}{y/z}={x/h(z),y/z} is our desired unifier.
page 128, the second paragraph of Section 12, line 3: If it contains a variable in one of the expressions, we can replace ...