I am grateful to Jørgen Villadsen for finding these errata (except as otherwise noted).

• Page 5 line 9: Since 51 is not prime, change to 102=5+97 (thanks to Robby Lampert).
• Page 12: The word "expression" in the first line of Section 2.2 should be italicized (thanks to Robby Lampert).
• Page 20, example 2.20: Replace not-q -> not-p with not-p -> not-q in the final line (thanks to Je-Min).
• Page 20, line -5: Missing symbols in v(B_1{A<-A'}) (thanks to Adam Dziedzic).
• Page 26, example 2.31. The example is correct, but a better example of an unsatisfiable formula would be U2 = {p, not p v q, not q}.
• Page 51, line -1: Section 3.6 should be Section 3.4.
• Page 102 last bullet: The second sentence is not correct, and should be changed to: "A closed formula has a model if and only if a certain formula constructed from it has a Herbrand model; consequently, to check for satisfiability, it is sufficient to check if there is a Herbrand model for this derived formula." (Thanks to Rick Greer.)
• Page 108, Figure 5.2, the sixth formula from the bottom has an extra parenthesis at the start of the line (thanks to Rick Greer.)
• Page 108, Figure 5.2, the fifth formula from the bottom is missing a parentheses (\forall x A(x) \vee \forall x B(x)) ... (thanks to Adam Dziedzic).
• Page 114, line 8: If there are no constants in U(l), let a be an arbitrary constant. This is mentioned in the informal discussion (p. 112, line 2) and in the systematic algorithm (p. 116, line 4), but not here. (Thanks to Alfredo Gabaldon.)
• Page 130, Theorem 6.7 should read: The deduction rule is a sound derived rule.
• Page 133-134: The discussion of the C-rule has several errors. (1) It is a new rule, not a derived rule. (2) In the third line, "c" should be "a". (3) In Theorem 6.22, "A" cannot contain any constant introduced by the C-rule. (4) Again in the Theorem, each use of the C-rule must introduce a new constant. See pages 73-75 of Mendelson (1964) for a good presentation of the rule.
• Page 138, exercise 7: The symbol for "provable" in the middle of the formula should be "implies".
• Page 143, lines 8-9: should be "A is logically equivalent to A', meaning ..." (thanks to Adam Dziedzic).
• Page 144, lines 7, 12: there is an extra parenthesis at the end of the formula (thanks to Dan True).
• Page 150 lines -7 and -9: the angled brackets should be parentheses.
• Page 154, last line of Example 7.32: The first formula should be "p(y) v q(f(y))" since only "x" is being substituted for "y" in the first step. (Thanks to Eduardo Zambon.)
• Page 178, definition 8.10: It is confusing that the same subscript "i" is used both to index the steps of the resolution and as the index of the literal within a goal clause that is used in a resolution step. The latter should be replaced by another variable such as "j". In fact, double indices should be used on both the A's and the B's to emphasize that the goal clauses and the program clauses at each step can be different.
• Page 183, line -3: "x" should be upper case.
• Page 184, line 14: "A+1" should be "List - List * Discount / 100".
• Page 237 line -5: "S" should be "\mathcal{S}".
• Page 239, line -3: The final comma should be a period.
• Page 300: The entry for "consistent" should be: "Consistent, maximally consistent set, 65" (thanks to Radovan Novakovic).

• The last number in the answer to exercise 13 of chapter 2 should be 11 not 8. (Thanks to Joerg Schneider.)

Last update 23 October 2011.