1, line -7: replace s(s(s(0))+0) by s(s(s(0)+0)). (Sebastian Skalberg) (p)
27, line -14 and -18: replace "bool" by "order" in the type of the ML functions "rem1" and "mdiff". (Stephen Eldridge) (p)
29, line 1: replace "example" by "examples". (Markus Triska) (p)
39, line 7: replace $\cal T$ by T. (Amine Chaieb) (p)
51, line 6: replace T by $\cal T$ (in the range of the homomorphism). (Sebastian Skalberg) (p)
52, line -15: replace X by V. (Amine Chaieb) (p)
60, Exercise 4.2: add "finite" before E. (Martin Lange) (p)
77, line 9: replace V(t) by Var(t). (Dennis Pagano) (p)
96, line -8: replace left-arrow over l by right-arrow. (Hisashi Kondo)
98, line 21 and 22: replace s1 by s0 (in definition of $\stackrel{\rightarrow}{\Gamma}$ and $\stackrel{\leftarrow}{\Gamma}$).
101, Exercise 5.2: replace "ground" by "right-ground". (Robert McNaughton) (p)
103, Exercise 5.6: Two assumptions are missing. First, the set of ground terms must be non-empty. Under this assumption, the order defined on p.104 is a reduction order. To show that it is the largest order, one must additionally assume that the order > one starts with is total on ground terms. (Ralph Matthes) (p)
111, Exercise 5.9: replace k|s|f by k(|s|f+1)
115, line 4: replace "variable" by "variable or a constant"
115-116: In the proof of Theorem 5.4.8 replace every occurrence of V(.) by Var(.).
120, lines 2 and 3: replace l by n. (Martin Lange) (p)
134-135, proof of Theorem 6.1.1: add the assumption "and neither l nor r is a variable" behind "Var(l) = Var(r)" (2 occurrences).
135: First sentence of section 6.2: insert "terminating" in front of "finite".
142: In Exercise 6.7 (b) replace both occurrences of E by G. (p)
153: line -2: replace "P1&ge" by "P1>". (Daniel Reiß)(p)
154: line 2: replace "P1&ge" by "P1>" and "P0&ge" by "P0>"; lines 3 and 4: replace "P0&le" by "P0<".
158: line -7: replace "canonical" by "convergent". (Philipp Lucas) (p)
183, line -13 (second recursive call of simpl): replace E by E'. (Jaco van de Pol) (p)
192, line 25 (penultimate line in proof of Theorem 8.2.7): replace fl by fs(l) (2 occurrences).
228, line -5: replace S1 by S (in exercise 10.3) (Sebastian Skalberg) (p)
239 and 242, in the displayed equation marked with (*): replace the 3x1 zero-matrix by the 1x1 zero-matrix "(0)". (Sebastian Skalberg) (p)
253, line 18: replace $\models s \not\approx t$ by $\not\models s \approx t$. (Sebastian Skalberg) (p)
255, line -15 through -11: The tau introduced locally with "Let tau be..." clashes with the global tau that occurs in the definition of sigma. It needs to be renamed to, for example, delta. Thus on those 5 lines all occurrences of tau, except for the 4th, 9th and 12th, should be replaced by delta. (Sebastian Skalberg) (p)