- P. 4, line 21: "which the required properties" should be "with the required properties". (Thanks to Antonio Prado.)
- P. 113, lines 9, 11: C should be C'.
- P. 113, Example 6.7: both occurrences of "\bar{q}p" should be "\bar{p}q".
- P. 118, line 5: The second 1 \leq i \leq 4 should be 1 \leq j \leq 4.
- P. 118, lines -9, -10: The indices for the formulas below i and j should be: (i+1,j+1), (i+1,j+2), (i+1,j+3), (i+1,j-1), (i+1,j-2), (i+1,j-3).
- p. 139, Definition 7.26: The three occurrences of S should be U. (Thanks to Hagit Shatkay.)
- P. 144-145: "\exists\neg xq(x)" should be "\exists x\neg q(x)". This occurs several times because of cut-and-paste :-(. (Thanks to Jørgen Villadsen.)
- p. 144, line 13: "element c such that c \in R_q" should be "element c such that c \not\in R_q". (Thanks to Hagit Shatkay.)
- P. 145, line 6 of Example 7.34: delete the extra parenthesis in "\exists x\neg p(x))". (Thanks to Andreas Schmidt Jensen.)
- P. 203: In Exercise 10, the reference is to the equivalences in Section 7.4.1. (Thanks to Jørgen Villadsen.)
- P. 224: A two-register machine needs an extra instruction such as an unconditional jump; alternatively, three registers can be used. In either case, the modifications to the proof of Church's Theorem are straightforward. The reference (Section 7.8) given in the proof of Theorem 1.2 is to the 1979 edition of Hopcroft and Ullman; in later editions, the proof is in Section 8.5. (Thanks to Thomas Bolander.)
- P. 332, line 6: x, y, z must be non-zero. (Thanks to Johan Öman.)
- P. 332, line 14: \mathcal{R} should be R. (Thanks to Rouven Walter.)
- P. 333, line 10: \mathcal{S}q should be \mathcal{SQ}. (Thanks to Rouven Walter and Jørgen Villadsen.)
- P. 333, line 17: "cardinality of a S" should be "cardinality of a set S." (Thanks to Rouven Walter.)
- P. 335, line 13: \mathcal{S} should be S. (Thanks to Rouven Walter.)
- P. 335, line -10: "consider" should be "considered".(Thanks to Jørgen Villadsen.)
I would like to thank Mohammad Najafian for finding the following typos:
- p. viii, line 13: "Important application" should be "Important applications".
- p. 5, line 13: "an result" should be "a result".
- p. 7, line -3: "out the main" should be "our main".
- p. 10, line -7: (\neg q) -> (\neg p) should be (\neg p) -> (\neg q).
- p. 12, line -1: "right formulas" should be "right formula" .
- p. 13, line 13: "holds all atoms" should be "holds for all atoms".
- p. 13, line -9: "in terms negation" should be "in terms of negation".
- p. 14, line 5: "Formula in propositional logic" should be "Formulas in propositional logic".
- p. 17, line -8: "supposed that" should be "suppose that".
- p. 25, line 9: the second formula should start in the second column.
- p. 29, line -5: "interpretation v" should be "interpretation I".
- p. 30, line -10: "an decision procedure" should be "a decision procedure".
- p. 33, line 4: "The set of formulas U" should be "The formulas in U".
- p. 35, line 9: "both set of literals" should be "both sets of literals".
- p. 39, line -17: "a purely formal" should be "purely formal".
- p. 47, line -12: "an adequate sets" should be "an adequate set".
- p. 56, line 8: "it will always clear" should be "it will always be clear".
- p. 77, line 17: "an logically equivalent" should be "a logically equivalent".
- p. 77, line -1: "A clause if trivial" should be "A clause is trivial".
- p. 82, line -12: "the this section" should be "this section".
- p. 85, line -14: "leave it to the read" should be "leave it to the reader".
- p. 121, line 2: "we can written" should be "we can write".
- p. 124, line 3: "on the these atoms" should be "on these atoms".
- p. 137, line 2: "less than" should be "less than or equal to".
- p. 144, line -5: "which to be expected" should be "which is to be expected".
- p. 146, line 14: "the construction the tableau" should be "the construction of the tableau".
- p. 170, line -4: "set of rational" should be "set of rational numbers".
- p. 174, line 16: "because since" should be "because".
- p. 186, line -5: "one function symbols" should be "one function symbol".
- p. 198, line -7: "there must be a substitutions" should be "there must be a substitution".
- p. 198, line -3: "there must subtitutions" should be "there must be substitutions".
- p. 211, line 8: "let use work" should be "let us work".
- p. 216, line 6: "which the branch taken" should be "which branch was taken".
- p. 218, line 6: "to enable it become" should be "to enable it to become".
- p. 223, line -8: "halts on an blank tape" should be "halts on a blank tape".
- p. 223, line -6: "give us an decision procedure" should be "give us a decision procedure".
- p. 228, line -3: "would have be of no interest" should be "would be of no interest".
- p. 239, line 19: "a interpretation is obtained" should be "an interpretation is obtained".
- p. 241, line -9: "provides an method" should be "provides a method".
- p. 255, line -9: "an reachable MSCC" should be "a reachable MSCC".
- p. 260, line 3: "something eventually occur" should be "something eventually occurs".
- p. 260, line -6: "A open tableau" should be "An open tableau".
- p. 279, line 1: "is partial correct" should be "is partially correct".
- p. 283, line 4: "in terms the weakest precondition" should be "in terms of the weakest precondition".
- p. 298, line -14: "state of a concurrent programs" should be "state of a concurrent program".
- p. 298, line -3: "These seems" should be "This seems".
- p. 324, line 13: "particular easy to use" should be "particularly easy to use".
- p. 324, line -14: "the proof the invariants" should be "the proof of the invariants".
- p. 336, line -6: "that is holds" should be "that it holds".
Last update 8 November 2021.