This chapter on the theory and applications of rewriting with equations discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based programming and (equational and Horn-clause) theorem proving. Ordinary, associative-commutative, and conditional rewriting are covered.

Term graph rewriting is concerned with the representation of functional expressions as graphs, and the evaluation of these expressions by rule-based graph transformation. Representing expressions as graphs allows to share common subexpressions, improving the efficiency of term rewriting in space and time. Besides efficiency, term graph rewriting differs from term rewriting in properties like termination and confluence. This paper is a survey of (acyclic) term graph rewriting, where emphasis is given to the relations between term and term graph rewriting. We focus on soundness of term graph rewriting with respect to term rewriting, on completeness for proving validity of equations and for computing term normal forms, on termination and confluence, and on term graph narrowing.

This tutorial gives a coherent overview of the area of explicit substitution and some applications. The focus is on the operational or syntactic side of things, in particular this will not cover the areas of semantics and type systems for explicit substitution calculi. Emphasis is put on providing a universal understanding of the very different techniques used by various authors in the area.

Preprint.

Rewriting is a general paradigm for expressing computations in various logics, and we focus here on rewriting techniques in equational logic. When used at the proof level, rewriting provides with a very powerful methodology for proving completeness results, a technique that is illustrated here. We also consider whether important properties of rewrite systems such as confluence and termination can be proved in a modular way. Finally, we stress the links between rewriting and tree automata.

This paper describes the application of proof orderings -- a technique for reasoning about inference systems -- to various rewrite-based theorem-proving methods, including ordered completion and a proof by consistency procedure for proving inductive theorems.
(The on-line version is a pre-publication technical report.)

A gentle introduction to the theory and applications of rewriting with equations. It discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based (functional and logic) programming and (equational, first-order, and inductive) theorem proving. An extensive bibliography is included.
(The on-line version is better than the published one.)

Preprint.

This excellent survey stresses confluence properties, orthogonal systems, and completion. It includes exercises.
(The on-line version does not have the valuable diagrams.)

This is a comprehensive survey of the theory of rewriting.
(The on-line version is imprecise.)

Equations occur frequently in mathematics, logic and computer science. in this paper, we survey the main results concerning equations, and the methods avilable for reasoning about them and computing with them. The survey is self-contained and unified, using traditional abstract algebra.
Reasoning about equations may involve deciding if an equation follows from a given set of equations (axioms), or if an equation is true in a given theory. When used in this manner, equations state properties that hold between objects. Equations may also be used as definitions; this use is well known in computer science: programs written in applicative languages, abstract interpreter definitions, and algebraic data type definitions are clearly of this nature. When these equations are regarded as oriented "rewrite rules", we may actually use them to compute.
In addition to covering these topics, we discuss the problem of "solving" equations (the "unification" problem), the problem of proving termination of sets of rewrite rules, and the decidability and complexity of word problems and of combinations of equational theories. We restrict ourselves to first-order equations, and do not treat equations which define non-terminating computations or recent work on rewrite rules applied to equational congruence classes.