This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases, and Buchberger's algorithm. They present the main algorithms both informally and as programs in the functional language Standard ML (An appendix contains a quick and easy introduction to ML). Key chapters cover crucial algorithms such as unification and congruence closure in more depth and develop efficient Pascal programs. The book contains many examples and over 170 exercises. This is also an ideal reference book for professional researchers: results spread over many conference and journal articles are collected here in a unified notation, detailed proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.
Author(s): Franz Baader, Tobias Nipkow
Publisher: Cambridge University Press
Year: 1998
Language: English
Pages: 313
Contents......Page 5
Preface......Page 8
1. Motivating Examples......Page 12
1. Equivalence and reduction......Page 18
1. Basic definitions......Page 19
2. Basic results......Page 21
2. Well-founded induction......Page 24
3. Proving termination......Page 27
4. Lexicographic orders......Page 29
5. Multiset orders......Page 32
6. Orders in ML......Page 37
2. Multiset orders......Page 38
7. Proving confluence......Page 39
1. Commutation......Page 42
8. Bibliographic notes......Page 44
1. Terms, substitutions and identities......Page 45
2. Algebras, homomorphisms and congruences......Page 55
3. Free algebras......Page 58
5. Equational classes......Page 60
4. Equational Problems......Page 69
1. Deciding ≈_E......Page 70
2. Term rewriting systems......Page 72
3. Congruence closure......Page 73
4. Congruence closure on graphs......Page 76
5. Syntactic unification......Page 82
6. Unification by transformation......Page 84
7. Unification and term rewriting in ML......Page 90
8. Unification of term graphs......Page 93
1. A quadratic algorithm......Page 97
2. An almost linear algorithm......Page 99
3. The complexity of sharing......Page 101
9. Bibliographic notes......Page 102
1. The decision problem......Page 104
1. Undecidability of the general case......Page 105
2. A decidable subcase......Page 110
2. Reduction orders......Page 112
3. The interpretation method......Page 115
4. Simplification orders......Page 122
1. Polynomial simplification orders......Page 128
2. Recursive path orders......Page 129
3. Recursive path orders in ML......Page 133
4. Knuth-Bendix orders......Page 135
5. Bibliographic notes......Page 142
1. The decision problem......Page 145
2. Critical pairs......Page 146
3. Orthogonality......Page 156
4. Beyond orthogonality......Page 162
5. Bibliographic notes......Page 168
7. Completion......Page 169
1. The basic completion procedure......Page 171
2. An improved completion procedure......Page 175
3. Proof orders......Page 183
4. Huet's completion procedure......Page 189
5. Huet's completion procedure in ML......Page 193
6. Bibliographic notes......Page 195
1. The ideal membership problem......Page 198
2. Polynomial reduction......Page 200
3. Groebner bases......Page 204
4. Buchberger's algorithm......Page 207
5. Bibliographic notes......Page 209
1. Basic notions......Page 211
2. Termination......Page 213
1. The disjoint case......Page 218
2. The orthogonal case......Page 219
4. Combining word problems......Page 222
1. The key ideas......Page 223
2. The formal solution......Page 225
3. Correctness......Page 227
4. The implementation in ML......Page 231
5. Bibliographic notes......Page 233
10. Equational Unification......Page 234
1. Basic definitions and results......Page 235
1. A unification algorithm......Page 241
2. The decision problem......Page 245
3. Associative and commutative functions......Page 247
1. Terms as vectors and substitutions as matrices......Page 248
2. AC1-unification......Page 249
3. AC-unification......Page 252
4. Homogeneous linear diophantine equations......Page 256
4. Boolean rings......Page 261
1. Polynomials......Page 262
2. Unification......Page 264
3. Loewenheim's formula......Page 265
4. Why Loewenheim's formula works......Page 267
5. Successive variable elimination......Page 268
7. Boolean unification in ML......Page 270
5. Bibliographic notes......Page 273
1. Rewriting modulo equational theories......Page 276
2. Ordered rewriting......Page 278
3. Conditional identities and conditional rewriting......Page 280
4. Higher-order rewrite systems......Page 281
5. Reduction strategies......Page 282
6. Narrowing......Page 284
1. Basic definitions......Page 287
1. Types......Page 289
2. Compound expressions......Page 290
3. Function declarations......Page 291
2. Lists......Page 293
6. Exceptions......Page 294
Bibliography......Page 295
Index......Page 308
