There are errors in some of the programs; see the software archive for improved versions.

Errata remaining in sixth printing are in a separate file.

Errata in second through fifth printings.
I am grateful to Jørgen Villadsen for finding these errata (except as otherwise noted).

• Front cover: The diagram is supposed to be a BDD, so half of the edges should be dotted.
• Page viii: See my website (left arrow below) for more up-to-date links and information on the availability of supplementary material.
• Page 4 line -9: The last expression should be b := b - a (thanks to Burak Gurdag).
• Page 5 line 10: Should be "It is not known if ..." (thanks to Russ Aiman).
• Page 5 line -9: "descriptive" should be "declarative".
• Page 16 line 15: Exclusive or has the same precedence as equivalence (thanks to Martin Henz).
• Page 21: nand and nor are not associative (thanks to Malek Haroud).
• Page 45: The double negation of A should be in the alpha column and the A should be in the alpha sub 1 column (thanks to Arina Britz).
• Page 48: In definition 3.9, axiom 2 has an extra bracket at the beginning of the formula.
• Page 48: First line of the proof of 3.10 should be (A -> ((A->A)->A)) -> ... .
• Page 58 line -10: Theorem 2.34 was stated for finite U but here we need its generalization to an infinite set of formulas.
• Page 61 line 1: Add a right parenthesis at the end of the formula.
• Page 63 line 3: "consequence" should be "consequent".
• Page 67 last line: Figure 2.6 does not include the (obvious) equivalences for eliminating nand and nor (thanks to Martin Henz).
• Page 77 Lemma 4.43 only holds when there are at least two failure nodes.
• Page 90-91: The indices have been reversed. The next to the last sentence on p. 90 should be: "... by recursively performing this algorithm on the left (right) sub-BDD of bdd1 and on bdd2", and on the top of p. 91: "... by recursively performing this algorithm on bdd1 and on the left (right) sub-BDD of bdd2" (thanks to Arina Britz).
• Page 93 line 6: "retraceall" should be "retractall".
• Page 101 line -6: "Sq and Pr" should be "Pr and Sq".
• Page 101 line -5: Of course "Pr(2)=F" should be "Pr(2)=T"!
• Page 102 line -8: "Chapter 8" should be "Chapter 7".
• Page 102 and elsewhere: "an Herbrand" should (probably) be "a Herbrand".
• Page 105, lines 5-6: these are not assignments, but relations and elements corresponding to the symbols (thank to Moonzoo Kim).
• Page 105, line -8: {d1,...,dn} should be (d1,...,dn) because these are sequences, not sets (thank to Moonzoo Kim).
• Page 107 line -6: "substitution" should be "consequence".
• Page 109, example 5.23: The next to the last sentence should have T instead of F (thanks to Arina Britz).
• Page 116 line 2: "singe" should be "single".
• Page 116: The first rule (line 7) of Algorithm 5.29 should read: "Check if U(l) contains a complementary pair of formulas. If so, mark the leaf as closed" (thanks to Martin Henz).
• Page 120 line 5: Both occurrences of "v" should be "or".
• Page 121, beginning of 5.8: Church and Turing worked independently of each other.
• Page 123 line 7 and line 10: Remove extra parenthesis at the end of the formula.
• Page 124 line 15: "satisfiable" should be "satisfiability".
• Page 129 line -10: "rules inference" should be "rules of inference".
• Page 132 line 9: Add ")" after first B(x) and delete after second B(x).
• Page 132 rule 6.15: "A(x) -> B(x)" should be "A(a) -> B(a)".
• Page 134 line -1: "member" should be "member_term".
• Page 136 line 7-8: Add a clause: "Number theory, first developed by Dedekind and Peano, is a".
• Page 143 line 12: "validity and satisfiability" should be "satisfiability and unsatisfiability".
• Page 146: Clauses for skolem should not include "imp" since the formula is assumed to be in CNF.
• Page 147 line 10: "the the" should be "the".
• Page 147 line 10: "[(X, (f, Z)), (Y, (g, U, W)]" should be "[(X, (f, [Z])), (Y, (g, [U, W]))]".
• Page 147 line -6: "One" should be "On".
• Page 149 line -2: "paf(f(a),a))" should be "paf(a,f(a,a))".
• Page 151 line -14: "build" should be "built".
• Page 157 line 6: "If x occurs in t" should be "If x occurs in t and x differs from t".
• Page 158 line -13: "rule 2" should be "rule 3".
• Page 159 Example 7.43: x = g(y) should go to the end of the queue.
• Pages 160, 161, 199, 200, 304 (index): "occur check" should be "occurs-check".
• Page 163 lines 4, 7, 20: In ISO Prolog, the use of =.. requires a prior check that the left operand is "nonvar".
• Page 182-183: The variables x,y,z should be capitals in all cases.
• Page 183 line 3: p should be teletype font.
• Page 183 lines 8-9: The answers will not be printed without explicit print statements.
• Page 184 line 11: Expression is unified with Result so it need not be an uninstantiated variable, although it usually is.
• Page 195 line 6: "select(Numbers, Head, NewNumbers)" should be "select(Head, Numbers, NewNumbers)".
• Page 196 line -15: "select(Numbers, Queen, NewNumbers)" should be "select(Queen, Numbers, NewNumbers)"
• Page 199 exercise 1: "identity substitution" should be "empty substitution".
• Page 200 line -5: Delete the sentence in parentheses.
• Page 204 line -4: Change sentence to: "Similarly, ... x := y+6 ... becomes y \le 1" (thanks to Martin Henz and Kooi Fei Foong).
• Page 236 line -12: "1965" should be "1959".
• Page 240 line -10: "If \tau linear" should be "If \tau is linear".
• Page 245 line 15-16: The leaf should be marked closed if it contains a complementary pair of literals, regardless of whether all formulas are literals.
• Page 246 line 7: "if all leaves are marked closed" should be "if all leaves are marked closed and there are no cycles".
• Page 246-247: The diagrams in 11.22 and 11.27 use a simple optimization of the algorithms.
• Page 247 line 1: "open semantic tableau" should be "open tableau without an open branch (hence there is a cycle)".
• Page 248 line -3: "A similar requirement must imposed" should be "A similar requirement must be imposed".
• Page 250 (figure): Reverse the arrows between s4 and s5 and between s6 and s7.
• Page 252 line 17: "If not, construct" should be "If not, then if there is an open branch then A is satisfiable; otherwise construct".
• Page 258 line 4 of the proof of 12.3: "Generalization" should be "Distribution".
• Page 262, line 2 of the proof of 12.18: "... because all its terminal MSCCs are non-fulfilling and were deleted".
• Page 264 lines 13-14: "but it shows that systematic proof that can be discovered" should be "but it shows that a systematic proof can be discovered".
• Page 274 and 279: The "Implementation" subsections should have a superscript P, while on p. 277, "Symbolic model checking" need not be starred since the entire section is.
• Page 280 exercise 3: Proving the validity of Axiom 6 is intended for those who have read the starred Section 12.3.
• Page 291 line -9: "analytic tableaux" should be "tableaux".
• Page 292 line -4 and page 294 line 1: "Creswell" should be "Cresswell".
• Page 293 line -8: "davis-putnam" should be "Davis-Putnam".
• Page 300: The entry for "consistent" should be: "Consistent, maximally consistent set, 65" (thanks to Radovan Novakovic).
• Page 300: "Horn clause" should include page 176.
• Page 301: Entries with Löwenheim are misplaced.
• Back cover line 4: "a elegant" should be "an elegant".
  See my website for more up-to-date links and information on the availability of supplementary material.

Errata for first printing, corrected in second printing.

• Page 69, line 8: "generalizaed" should be "generalized". (Thanks to Martin Henz.)
• Page 69: The last phrase of Example 4.10 should read: "S evaluates to F and S' evaluates to T". (Thanks to David Clark.)
• Page 106: The semantic definitions (validity, etc.) for the predicate calculus are given for closed formulas only, since: "... there is rarely any need to consider non-closed formulas...". A statement should have be added saying that all formulas in the text are considered closed unless otherwise noted. This is important for Section 5.5: The validity of a formula has been defined for closed formulas only, and the semantic tableau constructions are for closed formulas. However, the word closed is not mentioned. (Thanks to Mark Lawson.)
• Page 113-116: Algorithms 5.26 and 5.29 must be modified to include: If U(l) consists only of literals and gamma-formulas, check if there is a complementary pair of literals. If so, mark the leaf closed. An instructor may want to assign an analogue of Ex. 14 of Chapter 2: prove that the methods remain sound and complete if a leaf is declared closed if it contains any pair of complementary formulas. (Thanks to Mark Lawson.)
• Page 117: Hintikka's Lemma is Lemma 5.33, not Theorem 5.32.
  
• Page 134: Because of the way Generalization is defined, Theorem 6.22 should be as follows:
  
  Theorem 6.22 If U \- A using the C-Rule, then U \- A without using the C-Rule, provided that Generalization is not used on a formula containing a constant introduced by the C-rule.
  
  Furthermore, there are typographical errors in the proof of Theorem 6.23. In line 4, ExA(a,x) should be ExA(x,b) and in line 5, AyExA(y,x) should be AyExA(x,y).
  
• Page 140, 142: Either in Def. 7.4 or Def. 7.9, literals should be redefined (see Def. 5.25) to include non-ground formulas.
• Page 184, line 13: The program is not illegal, simply incorrect. The attempt to unify a second time will simply fail. (Thanks to Krzysztof Apt.)
• Page 264: In Theorem 12.20, the q's should be B's.
• Page 269: In the statement and proof of Lemma 12.26(b) and (c), add an additional disjunct Reset1 and Reset2, respectively. This change must also be made in line 2 of the proof of Lemma 12.17.
• Page 275 and 276: Node 12 is inconsistent and should be dropped from the text and from Figure 12.6.

Exercises:

• Chapter 6, exercise 8. "Prove that \-A iff \-A'" should be "Prove that \-A iff \- neg A'".
• Chapter 10, exercise 1. Delete this exercise as it refers to material in the first edition of the book.
• Chapter 10, exercise 2. There should be spaces between the functions and the arguments; in addition, in the definition of concatenation, 2..#t should be 1..#t.
• Chapter 11, exercises 3, 4, 5. The formulas that characterize models should have formula letters A, not propositional letters p, as in Section 11.3.
• Chapter 11, exercise 4. You can also assume that the relation is reflexive, that is, that \box A imples \box\box A is true.
• Chapter 11, exercise 9. The notation refers to the first edition of the book. The exercise should read: "Give a complete list of the elements of the four states in the structure in Figure 11.2."
• Chapter 12, exercise 1. The first formula is Theorem 12.4.
• Chapter 12, exercise 9. The forward direction of the second formula is not true in general, only at the origin.