## Table of Contents

*Preface*

**1 Motivating Examples**

**2 Abstract Reduction Systems**
2.1 Equivalence and reduction
2.1.1 Basic definitions

2.1.2 Basic results

2.2 Well-founded induction

2.3 Proving termination

2.4 Lexicographic orders

2.5 Multiset orders

2.6 Orders in ML
2.6.1 Lexicographic orders

2.6.2 Multiset orders

2.7 Proving confluence
2.8 Bibliographic notes

**3 Universal Algebra**
3.1 Terms, substitutions, and identities

3.2 Algebras, homomorphisms, and congruences

3.3 Free algebras

3.4 Term algebras

3.5 Equational classes

**4 Equational Problems**
4.1 Deciding =_{E}

4.2 Term rewriting systems

4.3 Congruence closure

4.4 Congruence closure on graphs

4.5 Syntactic unification

4.6 Unification by transformation

4.7 Unification and term rewriting in ML

4.8 Unification of term graphs
4.8.1 A quadratic algorithm

4.8.2 An almost linear algorithm

4.8.3 The complexity of sharing

4.9 Bibliographic notes

**5 Termination**
5.1 The decision problem
5.1.1 Undecidability in the general case

5.1.2 A decidable subcase

5.2 Reduction orders

5.3 The interpretation method

5.4 Simplification orders
5.4.1 Polynomial simplification orders

5.4.2 Recursive path orders

5.4.3 Recursive path orders in ML

5.4.4 Knuth-Bendix orders

5.5 Bibliographic notes

**6 Confluence**
6.1 The decision problem

6.2 Critical pairs

6.3 Orthogonality

6.4 Beyond orthogonality

6.5 Bibliographic notes

**7 Completion**
7.1 The basic completion procedure

7.2 An improved completion procedure

7.3 Proof orders

7.4 Huet's completion procedure

7.5 Huet's completion procedure in ML

7.6 Bibliographic notes

**8 Gröbner Bases and Buchberger's Algorithm**
8.1 The ideal membership problem

8.2 Polynomial reduction

8.3 Gröbner bases

8.4 Buchberger's algorithm

8.5 Bibliographic notes

**9 Combination Problems**
9.1 Basic notions

9.2 Termination

9.3 Confluence
9.3.1 The disjoint case

9.3.2 The orthogonal case

9.4 Combining word problems
9.4.1 The key ideas

9.4.2 The formal solution

9.4.3 Correctness

9.4.4 The implementation in ML

9.5 Bibliographic notes

**10 Equational Unification**
10.1 Basic definitions and results

10.2 Commutative functions
10.2.1 A unification algorithm

10.2.2 The decision problem

10.3 Associative and commutative functions
10.3.1 Terms as vectors and substitutions as matrices

10.3.2 *AC1*-unification

10.3.3 *AC*-unification

10.3.4 Homogeneous linear diophantine equations

10.4 Boolean rings
10.4.1 Polynomials

10.4.2 Unification

10.4.3 Löwenheim's formula

10.4.4 Why Löwenheim's formula works

10.4.5 Successive variable elimination

10.4.6 Complexity

10.4.7 Boolean unification in ML

10.5 Bibliographic notes

**11 Extensions**
11.1 Rewriting modulo equational theories

11.2 Ordered rewriting

11.3 Conditional identities and conditional rewriting

11.4 Higher-order rewrite systems

11.5 Reduction strategies

11.6 Narrowing

*Appendix 2 *** A Bluffer's Guide to** ML
*A2.1* Types

*A2.2* Expressions
*A2.2.1* Basic values

*A2.2.2* Compound expressions

*A2.3* Function declarations

*A2.4* Standard functions
*A2.4.1* Booleans

*A2.4.2* Lists

*A2.5* Datatypes

*A2.6* Exceptions