
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 KnuthBendix completion procedure and its variations, as well as
rewritingbased programming and (equational and Hornclause) theorem
proving. Ordinary, associativecommutative, and conditional
rewriting are covered.

Term Graph Rewriting
Detlef Plump.
Research Report CSIR9822, 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 rulebased 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, LS963, 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
JeanPierre Jouannaud.
In Proof and Computation, H. Schwichtenberg, ed.,
NATO series F: Computer and Systems Sciences, vol. 139,
pages 173218, 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):236276 (Feb. 1994).
This paper describes the application of proof orderings  a
technique for reasoning about inference systems  to various
rewritebased theoremproving methods, including ordered completion
and a proof by consistency procedure for proving inductive
theorems.
(The online version is a prepublication technical report.)

A Taste of Rewriting
Nachum Dershowitz.
Functional Programming, Concurrency, Simulation
and Automated Reasoning, Lecture Notes in Computer Science 693,
pages 199228, Springer (1993).
A gentle introduction to the theory and applications of rewriting
with equations. It discusses the existence and uniqueness of normal
forms, the KnuthBendix completion procedure and its variations, as
well as rewritingbased (functional and logic) programming and
(equational, firstorder, and inductive) theorem proving. An
extensive bibliography is included.
(The online 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 273364, 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 1117, Oxford University Press (1992).
This excellent survey stresses confluence properties, orthogonal
systems, and completion. It includes exercises.
(The online version does not have the valuable diagrams.)

Rewrite Systems
Nachum Dershowitz and JeanPierre Jouannaud.
Chapter 6 of
Handbook of Theoretical Computer Science B: Formal Methods and Semantics,
J. van Leeuwen, ed., pages 243320, NorthHolland (1990).
This is a comprehensive survey of the theory of rewriting.
(The online version is imprecise.)

Equations and Rewrite Rules  A Survey
Gérard Huet and Derek C. Oppen.
Research Report, STANCS80785, 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 selfcontained 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 firstorder equations, and do not
treat equations which define nonterminating computations or recent
work on rewrite rules applied to equational congruence classes.
Realized by
Nachum Dershowitz
and
Laurent Vigneron.
Last modified: 6Jan2005.