- Page 5, "if it occurs syntactically within G," should be "F" [Kwanghoon Choi]
- Page 33, Exercise 1.3: final \vee ("or") should be a \wedge ("and") [Eric]
- Page 49, Examples 2.21; page 50, Example 2.23: Line 3 of the first proof (and similarly for the others) is both unnecessary and not according to an inference rule listed in the book. Instead, split on line 2 and proceed.
- Chapter 4: Every use of T_\cons should be T_\cons^+ (the theory of acyclic lists).
- Page 66, top: In the final characteristic formula, F should be \neg F [Mathias Preiner]
- Page 68, Exercise 2.3 (e): \exists y. G should be \exists x. G to avoid capturing a free variable y in G
- Page 86, bottom: The axiom should specify that car(x) = x and cdr(x) = x [Roberto Sebastiani]
- Page 88: "where is has value w" should be "where it has value w" [ThanhVu Nguyen]
- Page 98, Example 4.2: \cons(d) should be d [Ben]
- Page 109, middle: "each possible formaulae" => "each possible formula" [Brandon]
- Page 109, Example 4.10: two instances of \vee should be \wedge (same issues as Exercise 1.3) [Zyad Hassan]
- Page 116, middle: should be "on the *right* half if a[m] < e and on the *left* half if a[m] > e" [Zyad Hassan]
- Page 136, bottom: Figure 5.22 should be referenced, not Figure 12.1 [Miquel Bertran]
- Page 151, Figure 5.25: "j" should be declared outside of the inner loop, and "t" should be included in r1 and r2
- Page 166, Figure 6.3: "a = a" in the construction of the qs instance should be "array = a"
- Page 167, Figure 6.4: the third row is incorrect, as the 5 and 6 are inverted [ThanhVu Nguyen]
- Page 188, bottom: x should be x' [Karl]
- Page 189, bottom: F should be F_4
- Page 197, top: F_5 actually has the form of a disjunction of such formulas [Yan Zhang]
- Page 202, second full paragraph: Every F_4 should be F_3
- Page 271, Example 10.3: Function and predicate symbols can
evaluate arbitrarily on tuples of D_J elements that include at least
one A element.
- Section 3.6, Chapter 11: The basic theory of arrays T_A should
include an axiom schema asserting that the domain is infinite: for
each positive integer n, forall x1, ..., xn. exists y. y != x1 &&
... && y != xn. This schema is unnecessary for arrays with integer
- Page 295, bottom: F should be F_3
- Page 305: Two additional axioms are required for the theory of hashtables: [Sebastien Bardin]
- keys-put 2: \forall h,j,k,v. j \ne k \rightarrow (j \in keys(put(h,k,v)) \leftrightarrow j \in keys(h))
- keys-remove 2: \forall h,j,k,v. j \ne k \rightarrow (j \not\in keys(remove(h,k,v)) \leftrightarrow j \not\in keys(h))