Errata for "Handbook of Practical Logic and Automated Reasoning"

If you discover a possible error that is not in this list, please let me know! You can email me at or find other contact information here. Unlike Knuth, I don't offer any payment, but you can enjoy the glory of appearing in this list and being acknowledged in any future edition of the book. I also welcome other suggestions and feedback, which may not appear here unless they are clear errors, but will still influence the future development of the book.

• page xi: The date of death for Thomas Hobbes given after the quotation should be 1679, not 1697. (Simon Similon.)
• page 10, in the discussion of syntax and semantics: the phrase "like algebraic manipulations" should not be in quotes.
• page 34, "As a simple example of ... structural induction ..., will show" should be "As a simple example of ... structural induction ..., we will show" (Jasmin Blanchette).
• page 39, first bullet in section 2.3: "if is satisfied by all valuations" should be "if it is satisfied by all valuations" (Samin Ishtiaq).
• page 50, psimplify function should have a clause to simplify Iff(False,False) to True, since as it stands one gets Not False (Roland Zumkeller and Sean McLaughlin).
  Here is a fixed version of the file prop.ml with this line added.
• page 102, third line from the bottom: "and if so returns one them together" should be "and if so returns one of them together" (Eric Taucher).
• page 119, in the second ML box, the power and cosine function are wrong way round so this doesn't match the formula above it is supposed to correspond to (Guillaume Melquiond).
  Here is a fixed version of the file fol.ml with this corrected.
• page 128, in the proof of Theorem 3.2, "holds M v p = not(holds M v p)" should be "holds M v p = not(holds M v q)" (Alan Crowe).
• page 130, second paragraph: "we usually just |= p" should be "we usually just write |= p"
• page 130, second line of section 3.4: the example of universal closure should be universally quantified over both x and z, not just x (Andreas Kübler).
• page 142, first displayed formula: to be consistent with the next page, this invalid formula should have a bar through the "iff" symbol (Anders Schlichtkrull).
• page 144, first paragraph of 3.6: Skolem's first name "Thoraf" should be "Thoralf" (Jasmin Blanchette).
• page 155, proof of Corollary 3.20: "... which is exactly Theorem 3.5" should say "... which is exactly Lemma 3.5" (Yasushi Fujiwara).
• page 166, middle of second paragraph of text: "complicated terms like x = g(f(g(y))" is missing a right parenthesis and should say "complicated terms like x = g(f(g(y)))" (Christoph Zengler).
• page 204, second line: "satisifes" should be "satisfies".
• page 205, first line of proof of Theorem 3.43: "right-to-left definition" should be "right-to-left direction".
• page 257: in the second rewrite example just above the "Abstract reduction relations" section, both instances of "a · c + b · d" should read "a · c + b · c" (Andreas Kübler).
• page 271: the term "local confluence" is used here and several more times but it was never explicitly stated that this is alternative terminology for "weak confluence" as defined earlier. Either the same terminology should be used everywhere or the definition on page 258 should mention both phrases (Tom Hales).
• page 317, top paragraph (last of section 5.3): there are actually 17 universal quantifiers not 19 using the code given in the book, and moreover the number of ground instances should be computed by raising that number to the tenth power, not vice versa. Thus "... has 19 universal quantifiers ... There are no fewer than "10¹⁹ ground instances" should be "... has 17 universal quantifiers ... There are no fewer than "17¹⁰ ground instances" (Andreas Kübler).
• page 321, definition 5.1: "valid in all finite models" should be "holds in all finite interpretations" (Tobias Nipkow).
• page 326: the penultimate paragraph uses R_M and plain R somewhat inconsistently. While not really likely to cause confusion, they are all with respect to the interpretation M so they should all, properly speaking, be R_M.
• page 329: "axiomatized by Σ and say that the theory is axiomatizable" should say "axiomatized by Σ, and say that the theory is recursively axiomatizable (confusingly, one often sees just axiomatizable) if there is a decidable or recursive set Σ that axiomatizes it (see section 7.5)". The footnote should probably also have a reference to exercise 7.11.
• page 332, line above displayed formula: "equivalence" should be "T-equivalence" or "equivalence in the theory of DLOs" (Tobias Nipkow).
• page 356, Corollary 5.12: this should explicitly state the assumption that we are working over an integral domain (Tom Hales).
• page 389, between first two displayed formulas: "theories defined by Horn clauses are convex (Theorem 3.39)" should be "theories defined by Horn clauses are convex (Theorem 3.43)".
• page 396, top line: q₁(x) = 0 \/ ... q_m(x) = 0 should be q₁(x) = 0 \/ ... \/ q_m(x) = 0.
• page 414, third line: "without affecting incompleteness" should be "without affecting completeness" or "without introducing incompleteness".
• page 449, first paragraph: ICS was based on Shostak, but Yices is actually based on Nelson-Oppen (Natarajan Shankar).
• page 451, near middle: "Soloray (private communication)" should be "Solovay (private communication)".
• page 457, exercise 5.10: should add "You may need to consider an expanded language" (Tobias Nipkow).
• page 459, exercise 5.25: this construction only results in a field extension where each polynomial with coefficients in the original field F has a root. To give the full algebraic closure of F one would need an iterative version of the construction (Tom Hales).
• page 489, second sentence of "Basic equality properties" section: "others properties" should be "other properties" (Anders Schlichtkrull).
• page 497, the OCaml type in the first paragraph should be "(term -> term) * fol formula -> thm" (Anders Schlichtkrull).
• page 504, second box: note that problem p58 is not in fact Pelletier problem 58, as the naming would suggest; in general, only those up to p46 correspond to Pelletier problems (Eric Taucher).
• page 531, near bottom of first subsection: "nested way inside term" should be "nested way inside a term".
• page 591, exercise 7.15: n_n ≠ 0 should be b_n ≠ 0.
• page 593, fourth line from bottom: "a inequation" should be "an inequation" (Eray Gençay).
• page 594, middle of page: "E[x] symbolizes" should be "anything of the form E[x] symbolizes" (Rune Fredriksen).
• page 594, fifth line from bottom: "pairs whose first member is in S and whose second member is in T, i.e. {(x,y) | x ∈ S and x ∈ T}" should say "... i.e. {(x,y) | x ∈ S and y ∈ T}" (William Denman).
• page 595, discussion below first list of relation properties: "the equality relation = has all properties other than irreflexivity" should say "... other than irreflexivity and connectedness" (Domenico Masini).
• page 597, on the second line of the second paragraph discussing characteristic functions, both instances of "f" should be "χ_S" (Vadim Flyagin).
• page 610, code in third box: the definition of odd should read "if n = 0 then false ..." rather than "if n = 1 then true ..." to ensure that it terminates for all nonnegative integers (Eray Gençay).
• page 626, last sentence: the whole sentence "This takes a flag ... existential" is incorrect and should simply be removed (Anders Schlichtkrull).
• page 629, first sentence: "use this is one" should be "use this as one" (Anders Schlichtkrull).
• page 638, Conway and Sloane reference: "Sloaue" in the volume editor should also be "Sloane".
• page 640, Dijkstra reference at the bottom of the page: the URL for the document www.cs.utexas.edu/users/EWD/ewd12xx/EWD1062.PDF should be www.cs.utexas.edu/users/EWD/ewd10xx/EWD1062.PDF (Eric Taucher).
• page 655, Mehlhorn et al. reference: "seel" should be "Seel" with an uppercase S.
• page 655, Melzer and Michi reference, "Melzer" should be "Meltzer".
• page 662, Smorynski (1980) reference: the title "Logic Number Theory" should be "Logical Number Theory"
• Not explicitly in the text but in the supplementary examples in the code. The Pelletier problem 27 is stated incorrectly, where "forall x. U(x) ==> ~R(x)" should read "forall x. V(x) ==> ~R(x)", and this appears in several places. One of the calls to isubst in "folderived.ml" is not given all its arguments.
  Here are fixed version of the files folderived.ml, lcffol.ml, meson.ml, resolution.ml and tableaux.ml with these corrected (Eric Taucher, Jørgen Villadsen).