Abstract
Equational reasoning is at the heart of many problems in automated
theorem proving, logic programming, program verification, program
synthesis, and symbolic computation. By its elegant and simple
formalism, term rewriting systems appear both as a powerful formal
concept and as an efficient mechanism to deal with these problems.
Two main applications are the equational reasoning in theorem provers
and equational computation in programming languages.
In equational logic, rewriting is a correct and complete deduction
inference rule as soon as the term rewriting system is confluent and
terminating. So, several rewriting laboratories, such as KB,
Reve, RRL, TRSPEC, LP, CEC or ERIL, have been designed to compute a
confluent and terminating set of rewrite rules from a set of
axioms. Then, rewriting was introduced in Horn clauses or first-order
theorem provers to handle equality efficiently. The notions necessary
for understanding how rewriting is used in different implementations
of theorem provers are presented in Section 2.
Beyond its use in algebraic specifications, for instance in ASF,
Asspegique or Axis, rewriting is also an evaluation mechanism
for programming languages based on equational logic, like OBJ, LOG(F)
or O'Donnell's language. Combining rewriting with a resolution-like
process gave rise to narrowing-based languages, such as SLOG or RAP.
Section 3 introduces the use of rewriting techniques in logic
programming languages.
In any implementation of rewriting techniques, efficiency is a crucial
issue. Section 4 sketches theoretical concepts and implemented
solutions for this problem.
Last but not least, a non-exhaustive catalog of distributed
implementations of term rewriting systems is presented. For each of
them, the underlying theoretical notions, presented in Sections 2, 3
and 4, are specified. We also give practical information on the
systems and, whenever they exist, references to practical examples of
their application.
Last modified: Tue Dec 2 20:50:51 MET