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 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 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 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 144, first paragraph of 3.6: Skolem's first name "Thoraf" should be "Thoralf" (Jasmin Blanchette).
• 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 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 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 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 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 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 638, Conway and Sloane reference: "Sloaue" in the volume editor should also be "Sloane".
• page 655, Mehlhorn et al. reference: "seel" should be "Seel" with an uppercase S.
• page 662, Smorynski (1980) reference: the title "Logic Number Theory" should be "Logical Number Theory"