There are errors in some of the programs; see the software archive for improved versions.
Errors in the second through fifth printings
Errors remaining in sixth printing are in a separate file that should also be consulted together with this list.
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 uptodate 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 9091: 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) subBDD of bdd1 and on bdd2", and on the top of p. 91: "... by recursively performing this algorithm on bdd1 and on the left (right) subBDD 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 56: 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 78: 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 "occurscheck".
 Page 163 lines 4, 7, 20: In ISO Prolog, the use of =.. requires a prior check that the left operand is "nonvar".
 Page 182183: The variables x,y,z should be capitals in all cases.
 Page 183 line 3: p should be teletype font.
 Page 183 lines 89: 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 1516: 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 246247: 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 nonfulfilling and were deleted".
 Page 264 lines 1314: "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: "davisputnam" should be "DavisPutnam".
 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".
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 nonclosed 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 113116: Algorithms 5.26 and 5.29 must be modified to include: If U(l) consists only of literals and gammaformulas, 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 CRule, then U \ A without using the CRule, provided that Generalization is not used on a formula containing a constant introduced by the Crule.
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 nonground 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.
Errors in the 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.
Last update 26 January 2011.