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
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
Explicit Substitution - Tutorial & Survey
Kristoffer H. Rose.
BRICS Lecture Series, LS-96-3, 150 pages, University of Aarhus,
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).
Rewrite Proofs and Computations
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
(The on-line version is a pre-publication technical report.)
A Taste of Rewriting
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).
Term Rewriting Systems
Jan Willem Klop.
Chapter 1 in Handbook of Logic in Computer Science,
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.)
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
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.
Last modified: 6-Jan-2005.