Surveys of Rewriting

• Rewriting

Nachum Dershowitz and David A. Plaisted. Chapter 9 in: Handbook of Automated Reasoning, vol. 1, A. Robinson and A. Voronkov, eds., 79 pages, Elsevier (2001).
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

Detlef Plump. Research Report CSI-R9822, 63 pages, Computing Science Institute, University of Nijmegen (Sep. 1998).
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.

• Explicit Substitution - Tutorial & Survey

Kristoffer H. Rose. BRICS Lecture Series, LS-96-3, 150 pages, University of Aarhus, (Sep. 1996).
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.

• Equational Logic Programming

Michael J. O'Donnell. Chapter 3 in: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 4, D. M. Gabbay, C. J. Hogger and J. A. Robinson, eds., 104 pages, Oxford University Press (1995).
Preprint.

• Rewrite Proofs and Computations

Jean-Pierre Jouannaud. In Proof and Computation, H. Schwichtenberg, ed., NATO series F: Computer and Systems Sciences, vol. 139, pages 173-218, Springer (1995).
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.

• Equational Inference, Canonical Proofs, and Proof Orderings

Leo Bachmair and Nachum Dershowitz. Journal of the ACM 41(2):236-276 (Feb. 1994).
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 Taste of Rewriting

Nachum Dershowitz. Functional Programming, Concurrency, Simulation and Automated Reasoning, Lecture Notes in Computer Science 693, pages 199-228, Springer (1993).
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.)

• Equational Reasoning and Term Rewriting Systems

David A. Plaisted. Chapter 5 in: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, D. Gabbay, C. Hogger, J. A. Robinson and J. Siekmann, eds., pages 273-364, Oxford University Press (1993).
Preprint.

• Term Rewriting Systems

Jan Willem Klop. Chapter 1 in Handbook of Logic in Computer Science, vol. 2, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, eds., pages 1-117, Oxford University Press (1992).
This excellent survey stresses confluence properties, orthogonal systems, and completion. It includes exercises.
(The on-line version does not have the valuable diagrams.)

• Rewrite Systems

Nachum Dershowitz and Jean-Pierre Jouannaud. Chapter 6 of Handbook of Theoretical Computer Science B: Formal Methods and Semantics, J. van Leeuwen, ed., pages 243-320, North-Holland (1990).
This is a comprehensive survey of the theory of rewriting.
(The on-line version is imprecise.)

• Equations and Rewrite Rules -- A Survey

Gérard Huet and Derek C. Oppen. Research Report, STAN-CS-80-785, 56 pages, Stanford University (Jan. 1980).
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.

Realized by Nachum Dershowitz and Laurent Vigneron.