Progress in Theoretical Computer Science

Editor
Ronald V. Book, University of California

Editorial Board
Erwin Engeler, ETH Zentrum, Zurich, Switzerland
Jean-Pierre Jouannaud, Universite de Paris-Sud, Orsay, France
Robin Milner, University of Edinburgh, Edinburgh, Scotland
Maurice Nivat, Universite de Paris VII, Paris, France
Martin Wirsing, Universitiit Passau, Passau, Germany
Leo Bachmair

Canonical
Equational
Proofs

1991 Birkhauser
Boston • Basel • Berlin
Leo Bachmair
Department of Computer Science
State University of New York at Stony Brook
Stony Brook, NY 11794
USA

Bachmair, Leo.
Canonical equational proofs / by Leo Bachmair.
p. cm. -- (Progress in theoretical computer science)
Includes bibliographical references and index.

1. Rewriting systems (Computer science) 2. Equations. I. Title.

II. Series.
QA267.B32 1991 91-11461
5113.3--dc20 CIP

Printed on acid-free paper.

© Birkhiiuser Boston 1991

Softcover reprint of the hardcover 1st edition 1991

All rights reserved. No part of this publication may be reproduced, stored in a retrieval
system, or transmitted, in any form or by any means, electronic, mechanical, photocopying,
recording, or otherwise, without prior permission of the copyright owner.

Permission to photocopy for internal or personal use of specific clients is granted by

Birkhiiuser Boston for libraries and other users registered with the Copyright Clearance
Center (CCC), provided that the base fee of $0.00 per copy, plus $0.20 per page is paid
directly to CCC, 21 Congress Street, Salem, MA 01970, U.S.A. Special requests should be
addressed directly to Birkhiiuser Boston, 675 Massachusetts Avenue, Cambridge, MA
02139, U.S.A.

3555-6/91 $0.00 + .20

ISBN-13:978-0-8176-3555-8 e-ISBN-13:978-1-4684-7118-2
DOl: 10.1007/978-1-4684-7118-2

Camera-ready text prepared in LaTeX by the author.

987654321
TO KARIN
Preface

Equations occur in many computer applications, such as symbolic compu-

tation, functional programming, abstract data type specifications, program
verification, program synthesis, and automated theorem proving. Rewrite
systems are directed equations used to compute by replacing subterms in a
given formula by equal terms until a simplest form possible, called a normal
form, is obtained. The theory of rewriting is concerned with the compu-
tation of normal forms. We shall study the use of rewrite techniques for
reasoning about equations.
Reasoning about equations may, for instance, involve deciding whether
an equation is a logical consequence of a given set of equational axioms.
Convergent rewrite systems are those for which the rewriting process de-
fines unique normal forms. They can be thought of as non-deterministic
functional programs and provide reasonably efficient decision procedures for
the underlying equational theories. The Knuth-Bendix completion method
provides a means of testing for convergence and can often be used to con-
struct convergent rewrite systems from non-convergent ones. We develop
a proof-theoretic framework for studying completion and related rewrite-
based proof procedures.
We shall view theorem provers as proof transformation procedures, so
as to express their essential properties as proof normalization theorems.
Applying this methodology to equational reasoning methods, we formu-
late the standard Knuth-Bendix completion procedure as an equational
inference system, the inference rules of which represent elementary compu-
tation steps that can be combined in different ways to yield a wide range
of specific completion procedures. The application of inference rules is
reflected by proof transformations on equational proofs and the goal of
completion is to deduce enough rewrite rules so that any equational proof
can be transformed to a normal-form proof, called a rewrite proof. We will
show how proof normalization results can be established via suitable order-
ings on equational proofs. This approach allows us to abstract from details
pertaining to the strategy controlling the inference mechanism. It facili-

Vll
Vlll

tates comparatively simple and intuitive correctness proofs and enable us

to characterize, via a notion of fairness, those strategies that yield correct
completion procedures.
We apply this inference system cum proof complexity approach to differ-
ent variants and refinements of completion, including critical pair criteria,
extended completion, and ordered completion. Furthermore, we discuss the
application of rewrite techniques to inductive theorem proving and describe
a method based on the concept of proof by consistency.
This monograph is based on the author's Ph.D. dissertation (submitted
to the University of Illinois at Urbana-Champaign in May 1987) and on
the following published papers: the inference system cum proof complexity
approach was first described in Bachmair, Dershowitz and Hsiang (1986);
critical pair criteria are discussed in Bachmair and Dershowitz (1988); ex-
tended completion is the topic of Bachmair and Dershowitz (1989); an
ordered completion procedure is presented in Bachmair, Dershowitz, and
Plaisted (1989); and the proof by consistency method is outlined in Bach-
mair (1988).

Acknowledgements
Most of the research was done while I was at the University of Illinois
at Urbana-Champaign and at the State University of New York at Stony
Brook. A preliminary version of the manuscript was prepared while I was
a visiting professor at the University of Nancy in the summer of 1988. The
work was also supported during various stages by the National Science
Foundation under grants DCR-8513417 and CCR-8901322.
I wish to take this opportunity to sincerely thank Nachum Dershowitz,
my thesis advisor. It has been a great pleasure to work with him.
I also like to thank Jean-Pierre Jouannaud, Jieh Hsiang, and David
Plaisted, who read most of the manuscript, for their valuable criticism.
I am grateful to all other colleagues and friends from whom I received
comments on various versions of part of this work. They include: Jiirgen
Avenhaus, Maria-Paola Bonacina, Bruno Buchberger, Jean Gallier, Harald
Ganzinger, Miki Hermann, Pierre Lescanne, Uday Reddy, Jean-Luc Remy,
Michael Rusinowitch, G. Sivakumar, Wayne Snyder, the students in my
seminars on rewriting, and anonymous reviewers.
Finally, I would like to thank Ron Book, the editor of this series, for his
patience.
Contents

Preface vii

1 EQUATIONAL PROOFS 1
1.1. Introduction. 1
1.2. Terms .. 5
1.3. Equations 6
1.4. Orderings 7
1.5. Proofs . . 9

2 STANDARD COMPLETION 13
2.1. Basic Completion . . . 14
2.2. Proof Transformation .. 16
2.3. Proof Simplification . . . 19
2.4. Fairness and Correctness. 20
2.5. Standard Completion. 25
2.6. Critical Pair Criteria . . . 31

3 EXTENDED COMPLETION 39
3.1. Rewriting Modulo a Congruence 40
3.2. The Left-Linear Rule Method 42
3.3. Church-Rosser Systems .. 47
3.4. Extended Completion . . . . 54
3.5. The Extended Rule Method. 55
3.6. Associative-Commutative Completion 60
3.7. The Protected Rule Method .. 65
3.8. Extended Critical Pair Criteria 69
4 ORDERED COMPLETION 73
4.1. Ordered Completion . . . . . . . . . . . . . . 75
4.2. Construction of Convergent Rewrite Systems 84
4.3. Refutational Theorem Proving . . . . . . . . 90

IX
x

4.4. Horn Clauses with Equality . 91

5 PROOF BY CONSISTENCY 99
5.1. Consistency and Ground Reducibility 99
5.2. Proof by Consistency. . . 101
5.3. Refutation Completeness. 107
5.4. Covering Sets . . . . . . . 111
Bibliography 117

Index 129
1. EQUATIONAL PROOFS

1.1. Introduction
Equations occur in many computer applications, such as symbolic compu-
tation, functional programming, abstract data type specifications, program
verification, program synthesis, and automated theorem proving. Rewrite
systems are collections of directed equations (rewrite rules) used to compute
by replacing subterms in a given formula by equal terms until a simplest
form possible (a normal form) is obtained. Many formula manipulation
systems, such as REDUCE or MACSYMA use equations in this manner. As
a computational formalism, rewrite systems have the full power of 'lUring
machines and various equational programming languages have been pro-
posed that are based on the paradigm of rewriting (e.g., O'Donnell 1985;
Goguen and Meseguer 1986). We shall study the application of rewrite
techniques to reasoning about equations.
The theory of rewriting is a theory of normal forms. Important proper-
ties of a rewrite system are termination, which guarantees the existence of
normal forms, and the Church-Rosser property, which ensures the unique-
ness of normal forms. Rewrite systems that enjoy both properties are
called convergent. They can be thought of as non-deterministic functional
programs.!
For example, the append operation on lists can be defined by the fol-
lowing equations:

app(nil,x) ~ x
app(cons(x, V), z) ~ cons(x,app(y,z))

The two equations define a convergent rewrite system. Any variable-free

term can be rewritten to a normal-form term built from the symbols cons
and nil. For example, we have

app( cons( a, nil), cons(b, cons( c, nil)))

- R cons(a, app(nil, cons(b, cons(c, nil))))
- R cons(a, cons(b, cons( c, nil)))

1 An important aspect of rewriting, which we will not discuss, is the efficient compu-
tation of normal forms; see the survey by Klop (1990b).

1
2 EQUATIONAL PROOFS

where R denotes the above rewrite system.

Another example of a convergent rewrite system is the following set of
equations:
ack(O, x) ~ S(x)
ack(S(x),O) ~ ack(x, S(O))
ack(S(x), S(y)) ~ ack(x, ack(S(x), y))
which defines Ackermann's function.
The characterization of free groups by the equations
e· x :;:::: x
x- . x :;:::: e
(x·y)·z ~ x . (y . z)
does not represent a convergent rewrite system, though. For instance, the
term (x-- . x-)· x has two different normal forms x-- . e and x.
Reasoning about equations may, for instance, involve deciding whether
an equation is a logical consequence of a given set of equational axioms.
Validity in theories axiomatized by (universally quantified) equations can
be characterized proof-theoretically: an equation s ~ t is true in all models
of a (countable) set of equations E if and only if it can be proved from
E by application of substitutions and replacement of subterms by equal
terms. Validity in equational varieties is thus semi-decidable. Convergent
rewrite systems provide decision procedures: an equation s ~ t is valid in
the equational variety described by a convergent rewrite system if and only
if sand t can be rewritten to identical normal forms. Deciding validity in
such theories is thus reasonably efficient.
Knuth and Bendix (1970) devised an effective test for deciding whether
a given terminating rewrite system is convergent. They also suggested a
method with which a convergent system can often be constructed from a
non-convergent one. 2 This completion procedure is supplied with a set
of equations and a well-founded ordering (a reduction ordering) which is
used to orient equations into rewrite rules. If a rewrite system is not con-
vergent, new equations (critical pairs) are deduced by a restricted version
of paramodulation, called superposition. More precisely, critical pairs are
obtained by paramodulating left-hand sides of rewrite rules into other left-
hand sides, with no paramodulations taking place within the variable part
of a rule. The given reduction ordering thus provides strong guidance to
the deduction mechanism and drastically limits the search space of equa-
tional consequences that need to be computed. (The functional reflexivity
axioms, which present a problem to many equational theorem provers, need
not be included either.)
2A convergent rewrite system for group theory is given in Section 2.2.
 INTRODUCTION 3

An intriguing feature of completion is that rewrite rules can be used

to simplify other, already deduced equations. That is, all terms can be
systematically rewritten to normal form by the current rewrite rules. As
a consequence, many redundant equations are discarded. While such sim-
plification accounts for the practicality of completion, it also complicates
the task of verifying that a procedure is correct (i.e., does in fact produce
a convergent rewrite system). We develop a proof-theoretic framework for
reasoning about completion and other rewrite-based deduction methods.
(Several such methods are outlined in Buchberger 1987.)
Theorem provers can often be viewed as proof transformation or proof
normalization procedures, and their essential properties can then be ex-
pressed as proof normalization theorems. We shall apply this approach to
rewrite-based equational reasoning methods and, in particular, will formu-
late completion as an equational inference system. The individual infer-
ence rules represent elementary computation steps of completion and can
be combined in different ways to yield a wide range of completion pro-
cedures. This approach allows us to abstract from details pertaining to
the strategy controlling the inference mechanism. The application of an
inference rule is reflected by certain proof transformations on equational
proofs and the goal of completion is to deduce enough rewrite rules so that
any equational proof can be transformed to a certain normal-form proof,
called a rewrite proof. We will show how proof normalization results can
be established via suitable orderings on equational proofs. Proof orderings
facilitate comparatively simple and intuitive proofs of correctness and en-
able us to characterize, via a notion of fairness, those strategies that yield
correct completion procedures.
In Chapter 2, we introduce the basic concepts of this inference sys-
tem cum proof complexity approach by applying it to the standard Knuth-
Bendix completion procedure. We present an abstract completion inference
system and prove the correctness of a wide class of completion procedures.
Furthermore, we utilize proof orderings in describing refinements of stan-
dard completion based on sorting out redundant critical pairs. These tech-
niques, which are called critical pair criteria, permit better control over the
number of equations generated and may considerably improve the efficiency
of completion.
Many equational theories cannot be represented as terminating (or con-
vergent) systems, e.g., theories containing commutativity axioms. Instead,
problematic axioms such as commutativity can often be built into the com-
pletion procedure itself via generalized matching and unification algorithms
and a corresponding notion of extended rewriting. Completion procedures
based on extended rewriting were first described for the case of associativ-
ity and commutativity. In Chapter 3, we describe these and other, more
4 EQUATIONAL PROOFS

general completion procedures by inference rules. We establish the cor-

rectness of various approaches to extended completion: the left-linear rule
method, the extended rule method, and the protected rule method. As a
special case, we discuss associative-commutative completion in some detail.
A brief discussion of extended critical pair criteria is also included.
Completion must be supplied with a reduction ordering which it uses to
orient equations into rewrite rules, and may fail if an equation is generated
that cannot be oriented. In fact, standard completion may fail even when
a convergent system exists and it is supplied with a suitable ordering! In
Chapter 4, we address this problem by presenting a method for dealing
with unorientable equations, called ordered completion, which is designed
to construct sets of equations that define unique normal forms for variable-
free terms only. This weaker normal-form property is sufficient in many
applications, such as refutational theorem proving. Ordered completion
is a refutation ally complete theorem prover for equational theories, but
has the advantage over paramodulation that terms can always be kept in
fully-simplified form and that fewer equational consequences need to be
considered, as the ordering supplied to the procedure gives some measure
of direction to the prover. Ordered completion is guaranteed to find a
convergent system, if one exists and the reduction ordering supplied to the
procedure satisfies some reasonable conditions. In the more general context
of Horn clauses with equality it yields an inference system consisting of
restricted versions of positive unit resolution and paramodulation (with
simplification) .
In many applications, such as algebraic data type specifications and
equational programming, equations are intended to define a certain stan-
dard model, called the initial model. This initial algebra semantics typically
requires proof methods that employ some induction schema, e.g., induction
on the structure of terms. In Chapter 5, we discuss an alternative approach
based on the concept of proof by consistency and apply it to equational the-
ories that are presented as rewrite systems defining unique normal forms for
variable-free terms. In contrast with so-called inductive completion proce-
dures, this proof by consistency method can handle unorientable equations.
The method is linear in that every deduction step involves one of the orig-
inal axioms. It is refutation ally complete in that it refutes any equation
which is not an inductive theorem.
We assume that the reader is familiar with the fundamental concepts of
term rewriting; a brief introduction is provided in the remaining sections of
this chapter. Our terminology is consistent with Dershowitz and Jouannaud
(1990). For further details on rewriting the reader may also consult the
surveys by Huet and Oppen (1980), Klop (1987, 1990a), and Avenhaus and
Madlener (1990).
 TERMS 5

1.2. Terms
Let :F and V be two disjoint (countable) sets. The elements of :F are called
function symbols; the elements of V, variables. With each function symbol
I we associate a non-negative number, called its arity. Function symbols
of arity 0 are called constants.
A term is either a variable or an expression It 1 ... tn, where I is a
function symbol of arity nand t 1 , .•• , tn are terms. The set of all terms built
from function symbols in:F and variables in V is denoted by T(:F, V). Terms
containing no variables are called ground terms. The set of all ground terms
is denoted by T(:F). To enhance readability, we shall often use parentheses
and infix notation. For example, we may write (S(x) + y) + 0 instead of
++SxyO. The term (S(x) + y) + 0 is non-ground, whereas S(O) + 0 is
ground.
A term s is said to be a subterm of a term t if either s = t, or else
t = It 1 ... tn and s is a subterm of one of the terms ti. By a proper
subterm oft we mean a subterm distinct from t.
We use sequences of positive numbers, also called positions, to refer to
specific subterms in a term. The empty sequence A is a position in any
term t, whereas a sequence ip is a position in a term t = It1 ... tn only if
1 ~ i ~ nand p is a position in ti. (The concatenation of two sequences
p and q is denoted by juxtaposition pq.) If p is a position in a term t then
the subterm tip of t at position p is t, if p = A, and td q, if t = It1 ... tn
and p = iq, for some i with 1 ~ i ~ n. We say that a position p is below
a position q (or q is above p) if p = qq', for some position q'. If q' is non-
empty, then p is said to be strictly below q (and q strictly above p). Two
positions are disjoint if neither one is below the other.
The result of replacing in t the subterm at position p by s is de-
noted by t[s]p and is defined to be the term s, if p = A, and the term
It1 '" ti-1ti[S]qti+1 ... tn, if t = It1'" tn and p = iq. More generally,
if P1, .. " Pn are pairwise disjoint positions, for some n ~ 2, we write
t[Sl, ... , Sn]Pl, ... ,Pn to denote the term (t[Sdpl )[S2, ... , sn]P2, ... ,Pn' We also
write t[s] to indicate that the term t contains s as a subterm, and (ambigu-
ously) denote by t[u] the result of replacing a particular occurrence of S in
t by u.
A substitution is a mapping from variables to terms. The value of
a substitution u for variable x is denoted by xu. A substitution u can be
uniquely extended to a mapping on terms in such a way that (ft1 ... tn)u =
1{t1u) ... (tnu), for all terms It1 ... tn. The composition of two substitu-
tions u and r is denoted by juxtaposition ur. That is, tur (tu)r for all=
terms t. We usually need to consider only substitutions for which xu = x
for all but a finite number of variables. By {Xl I--t t1,"" xn I--t t n } we
6 EQUATIONAL PROOFS

denote the substitution u for which xu = ti, if x = Xi, for some i with
1 ::; i ::; n, and xu = x, otherwise.
A term t is an instance of (or matches) another term s if t = SU, for
some substitution u. An instance t of S is said to be proper if s is not an
instance of t. Thus -x + 0 and x + x are proper instances of x + y, while
x + z is a non-proper instance. Two terms sand t are literally similar if
they are instances of each other. In other words, two terms are literally
similar if and only if they can be obtained from each other by a suitable
renaming of variables. The two terms x + y and x + z are literally similar,
but x + y and x + x are not.
Two terms sand t are said to be unifiable if there exists a substitution u,
called a unifier, such that su = tu. For example, the two terms Ix and Igy
are unifiable, whereas I x and gy are not. The two substitutions {x 1-+ gy}
and {x 1-+ 9 I z, Y 1-+ I z} are both unifiers of I x and I gy, though the first
unifier is more general than the second. More precisely, a unifier u of sand
t is said to be most general if for every unifier 7 (of sand t) there exists a
substitution 7' such that XU7' = X7, for all variables x. Unifiability of terms
is decidable. Furthermore, if two terms are unifiable, then they have a most
general unifier, which is unique up to renaming of variables. Algorithms for
computing the most general unifier of two terms (if one exists) have been
described by Robinson (1965), Paterson and Wegman (1978), and Martelli
and Montanari (1982). For a recent survey on unification see Jouannaud
and Kirchner (1990).

1.3. Equations
An equation is a pair of terms, written s ~ t. We are interested in various
congruence and rewrite relations induced by a given set of equations. An
equivalence relation 3 '" on terms is called a congruence if SI '" tl' ... '
Sn '" tn implies ISl ... Sn '" Itl ... tn, for all terms Sl, ... ,Sn, tb ... ,tn
and function symbols I of arity n. A binary relation -+ on terms is called
a rewrite relation if S -+ t implies u[su]p -+ u[tu]p, for all terms s, t, and u,
positions p in u, and substitutions u. Rewrite relations are often denoted
by arrows of one kind or another. If -+ is a binary relation, we denote by
- its inverse; by ....... its symmetric closure -+ U -; by -++ its transitive
closure; by -+* its transitive-reflexive closure; and by ....... * its symmetric-
transitive-reflexive closure.
If E is a set of equations, we write S -+ E t to indicate that there exist
a term w, a position p in w, a substitution u, and an equation u ~ v in
E, such that S = w[uu]p and t = w[vu]p. The relation -+E is called the

3 An equivalence relation is a reflexive, tranSitive, and symmetric binary relation.

 ORDERINGS 7

rewrite relation induced by E. We also say that s rewrites to t (in one step)
if s - E t. A term that cannot be rewritten is said to be in normal form or
irreducible (by E). A normal form of t (in E) is any irreducible term u for
which t -:E u. We write s -E t if either S -E t or t -E s.
The symmetric-transitive-reflexive closure -:E of - E is called the equa-
tional theory induced by E. We also say that two terms s and t are equiv-
alent in E if s -:E t. A set E of equations will be called a rewrite system if
the corresponding rewrite relation - E is the primary object of study. The
equations of a rewrite system are also called rewrite rules.

sand t with s -* t, there exists an element v such that s -*

A binary relation - is said to be Church-Rosser if for any two elements
v and v -*
t.
It is said to be terminating if there is no infinite sequence to - t1 - t2 ....
Terminating Church-Rosser relations are called convergent.
A rewrite system R is called convergent if the corresponding rewrite re-
lation - R is convergent. Convergent rewrite relations define unique normal
forms. Thus, if R is a finite convergent rewrite system, then equivalence of
terms in R is decidable: two terms are equivalent in R if and only if they
can be rewritten to identical normal forms.
Finally, a rewrite system R is said to be reduced if for all rewrite rules
s ~ t in R, the term s is irreducible by R \ {s ~ t} and t is irreducible by
R. Reduced convergent rewrite systems are often called canonical. They
are unique up to renaming of variables (Metivier 1983).

1.4. Orderings
An (strict partial) ordering is an irreflexive, transitive binary relation; a
quasi-ordering, a reflexive, transitive binary relation. For example, the
greater-than relation on the natural numbers is a strict ordering, while the
greater-than-or-equal-to relation is a quasi-ordering.
If >- is a strict ordering, then its reflexive closure t is a quasi-ordering.
On the other hand, if t is a quasi-ordering, the corresponding equivalence
"" and strict ordering >- are defined as follows: s "" t if s t t and t t s;
and s >- t if s t t and t ~ s. An ordering >- is called well-founded if it is
terminating. A quasi-ordering t is said to be well-founded if its strict part
>- is well-founded.
If h and >-2 are both orderings, than their lexicographic combination
is an ordering on pairs, defined by: (s,t) >- (s',t') if either s >-1 s' or
else s = s' and t >-2 t'. More generally, if t1 is a quasi-ordering, we
define: (s, t) >- (s', t') if either s >-1 s' or else s ""1 s' and t >-2 t', where
>-1 and ""'1 are the strict ordering and equivalence, respectively, associated
with t1. The lexicographic combination of more than two orderings (or
8 EQUATIONAL PROOFS

quasi-orderings) is defined in the obvious way. A lexicographic ordering is

well-founded if and only if all its component orderings are well-founded.
A multiset over a set S is a mapping M from S to the natural numbers.
Intuitively, M (x) specifies the number of occurrences of x in M. We say that
x is an element of M if M(x) > O. The union and intersection of multisets
are defined in the usual way by the identities M 1UM2(x) = M 1(x)+M2(x)
and M1 n M2(X) = min(M1(x), M2(X)). A multiset M is finite if the set
{x : M(x) > O} is finite. For simplicity, we often use a set-like notation to
describe (finite) multisets. For example, {x,x,x} denotes the multiset M
=
for which M(x) 3 and M(y) 0, for y:/: x. =
Any partial ordering >- on a set S can be extended to an ordering >-mul
on (finite) multisets over S as follows: M >-mul N if (i) M :/: N and (ii)
whenever N(x) > M(x) then M(y) > N(y), for some y such that y >- x. In
other words, according to the multiset ordering any element of a multiset
can be replaced by any finite number of smaller elements. Dershowitz and
Manna (1979) showed that the multiset ordering >-mul is well-founded (on
finite multisets) if and only if the ordering >- is well-founded.
A rewrite ordering is an ordering that is also a rewrite relation. Well-
founded rewrite orderings are called reduction orderings. We say that a
reduction ordering >- satisfies the subterm property ift[s] >- s, for all terms
t and proper sub terms s of t. Reduction orderings that satisfy the subterm
property are called simplification orderings.
A rewrite relation ---- R terminates if and only if the rewrite system R
is contained (as a subset) in some reduction ordering. If a convergent
rewrite system R is contained in a reduction ordering >-, then a term is
irreducible with respect to R if and only if it is minimal (with respect to
>-) in its equivalence class. The following orderings, which are based on
lexicographic or multiset orderings, are particularly useful for proving the
termination of rewrite relations.
Let f be a function symbol of arity n with which we associate a mapping
(called the status of f) that assigns to each ordering >- on terms an ordering
>-1 on n-tuples of terms. In particular, the function symbol f is said to
have multiset status, if >-1 is defined by: (Sl, ... ,5n ) >-1 (t1, ... ,tn) if
{51, ... , 5n } >-mul {t1, ... , tn}; while it is said to have lexicographic status
if there exists a permutation 7r of {1, ... ,n}, such that (51, ... ,5 n ) >-1
(t1, ... , tn) if (i) (5,..(1), ... , 5,..(n)) >-lex (t,..(l), ... , tx-(n)) and (ii) f 51 .. . 5n >-
t;, for all i with 1 SiS n. (Here >-lex denotes the n-fold lexicographic
combination of the ordering >-.)
Let >- be an ordering, called a precedence, on a given set of function
symbols, and suppose that each function symbol has either multiset or
lexicographic status. Then the corresponding recursive path ordering >-rpo
 PROOFS 9

is recursively defined by:

5 = f 51 ... 5 m >-rpo gt1 ... tn =t

if
Si ~rpo t, for some i with 1 ~ i ~ m,
or
f >- g and s hpo tj, for all j with 1 ~ j ~ n,
or
f = g and (51' ... ' Sm) >-!po (t1' ... ' t m )
(Kamin and Levy 1980).
A recursive path ordering is more specifically called a multiset path
ordering and denoted by >-mpo, if each function symbol has multiset status
(Dershowitz 1982a). A lexicographic path ordering >-lpo is a recursive path
ordering where each function symbol has lexicographic status with 7r being
the identity permutation.
For example, if * >- + in the given precedence, then (a + b) * c >-mpo
(a * c) + (b * c), as both (a + b) * c >-mpo (a * c) and (a + b) * c >-mpo (b * c).
The two terms (a+b)+c and a+(b+c) are not comparable in the multiset
path ordering, while (a + b) + c >-lpo a + (b + c).

Proposition 1.1. (Kamin and Levy 1980) Any recursive path ordering is
a simplification ordering if the underlying precedence on function symbols
is well-founded.

For a detailed discussion of termination orderings the reader may consult

the survey by Dershowitz (1987).

1.5. Proofs
Theorem provers can often be viewed as proof transformation or normaliza-
tion procedures. Such a theorem prover is said to be correct if enough conse-
quences can be deduced so that any arbitrary proof can be transformed to a
normal-form proof. We study rewrite-based equational reasoning methods
from this point of view. In this context, the set of theorems corresponds
to some congruence relation induced by a given set of equations; proofs
are finite sequences of equational replacements; and normal-form proofs
are those proofs in which equations are used in a specified direction, as
one-way rewrite rules.
10 EQUATIONAL PROOFS

In describing equational proof procedures, we shall assume that equa-

tions are labelled by non-negative numbers or the symbols ..1 or T. We
write s ~n t to denote labelled equations. 4
Definition 1.2. A (equational) proof step is an expression s ~ t, where
sand t are terms, e is an equation u ~n v, and p is a position in s, such that
sip = UO" and t =
s[vO"]p, for some substitution 0". We say that s ...... ~::= .. " t
is a proof step in E if either u ~n V or v ~n U is an equation in E.
Occasionally we will write s ~n t to ambiguously denote s ~n t or t ~n s.
Evidently, there is a proof step s ......~::= .. " t in E if and only if s ...... E t.
Definition 1.3. A (equational) proof (oft o ~ tn) is any finite sequence of
proof steps
to ~: tl, tl ~~ t2,···, tn-l ......~: tn,
usually written in abbreviated form,

The empty sequence serves as a proof of any "trivial" equation t ~ t.

The letters P and Q are used to denote proofs. We say that P is a proof
in E if each proof step of P is in E. An equation s ~ t is provable in E,
in this sense, if and only if s ...... :E t. For simplicity, we often denote by
s - E t any proof step s ......~::= .. " t, where u ~n V is an equation in E; by
s ~E t, a proof step s ......~::= .. " t, where v ~n U is an equation in E; and by
s ...... E t a proof step s - E t or s ~E t. We also write s ......:E t to denote
arbitrary proofs in E. A proof of the form s ~E u - E t is called a peak;
a proof to -:E tic ~:E tn, a rewrite proof.
If ei is an equation Ui ~Ic; Vi, for 1 ~ i ~ n, and P is a proof

we denote by p- l the proof

by PO" the proof

toO"~: tlO" ~~ t20"· ··tn-10" ......~: tno";

-----------------------
The labels allow us to make finer distinctions between equational proofs.
~ For in-
stance, we will employ labels to indicate whether an equation is to be used in a specified
direction as a (one-way) rewrite rule. All notions defined for unlabelled equations will
also be applied to labelled equations. For instance, when speaking of the rewrite relation
induced by a set of labelled equations E, we mean the rewrite relation induced by the
set of equations {s ~ t : s ~n tEE, for some n}.
 PROOFS 11

and by u[P]q, where q is a position in u, the proof

u[to]q +-+~~1 U[tl]q +-+~~2 U[t2]q ... U[tn-l]q +-+~~ .. u[tn]q.

If P is a proof (in E), then p- 1 , Pu, and u[P]q are also proofs (in E). We
speak of a ground proof if all terms to, ... ,tn are ground. By a subproof
of P we mean any proof

t •· +-+Pi+l t·+ ·· ·t·J -

ei+ 1 • 1
1 ~j t·
e j J'

where 0 ~ i ~ j ~ n. We write P[Q] to indicate that P contains Q as a

subproof, and denote by P[Q'] the proof obtained from P by replacing Q
by Q'. The composition of a proof P (of s :::::: t) and a proof Q (of t :::::: u) is
denoted by juxtaposition PQ (and is a proof of s:::::: u).

Definition 1.4. A proofrewrite relation is any binary relation ~ on proofs

such that (i) P ~ Q implies u[Pu]q ~ u[Qu]q, for all proofs P and Q,
substitutions u, terms u, and positions q in Uj and (ii) Q ~ Q' implies
P[Q] ~ P[Q'], for all proofs P[Q], Q, and Q'. If in addition (iii) P and Q
are proofs of the same equation whenever P ~ Q, then the proof rewrite
relation is called a (proof) transformation relation.
If a proof rewrite relation is a well-founded ordering, it is called a proof
reduction ordering (or simply proof ordering).
2. STANDARD COMPLETION

Knuth and Bendix (1970) proposed a procedure that attempts to transform

a given set of equations into a convergent rewrite system. This completion
procedure must be supplied with a reduction ordering, which determines
the direction in which an equation is to be oriented into a rewrite rule.
It deduces new equations by a process called superposition. An intriguing
feature of the procedure is that rewrite rules can be used to simplify other,
already deduced equations. Terms can therefore be kept in fully simplified
form and redundant equations can be discarded. Deduction and simplifi-
cation are the two main components of completion. While simplification
accounts for the practicality of completion, it also complicates the task of
verifying that a procedure is correct (i.e., does in fact produce a convergent
set of equations).
We reformulate the Knuth-Bendix completion method as an equational
inference system and demonstrate that completion can be viewed as a pro-
cess of proof simplification, the goal of which is to deduce enough rewrite
rules so that any equational proof can be transformed to a normal-form
proof, that is, a rewrite proof.
In this context, an inference rule is a binary relation on (finite) sets
of equations. The inference rules represent elementary computation steps
of completion. They can be combined in different ways to yield a wide
range of completion procedures. Each inference rule induces certain proof
transformations that can be described by rewrite rules on equational proofs.
We present well-founded orderings on proofs that can be used to establish
proof normalization results for (abstract) completion and related rewrite-
based proof methods.
In this chapter, equations are assumed to be labelled by one of the
symbols T or.L We usually leave the labels implicit. ~quations s ~l. t
are called rewrite rules and written s - t. We write E; 'R to denote a set
EUR, where E is a set of equations s ~T t and R is a set of rules s ~l. t. A
proof step s ..... E t is called an equality step; a proof step s - R tor S ..... R t,
a rewrite step.

13
14 STANDARD COMPLETION

2.1. Basic Completion

Let >- be a reduction ordering on terms. The inference system 8>- consists
of the following inference rules:

E;R
DEDUCTION:
EU{s:::::t};R

EU{s~t};R
ORIENTATION: ifs>-t
E;RU{s-+t}

EU{s:::::s};R
DELETION:
E;R
EU{s~t};R
SIMPLIFICATION: if S -+R u
EU{u~t};R

where E and R denote finite sets of equations, with R being contained in

the reduction ordering >-.
Inference systems 8>- are called basic completion systems. We usually
leave >- implicit and write 8 instead of 8>- .
In essence, new equations s ::::: t are obtained by rewriting some term u
in two different ways to s and t, respectively. Such equations are deduced
from R, but not from E. They serve to eliminate peaks s +-R u -+R t. As
we shall see, only equations obtained from so-called critical peaks (of which
there are only finitely many, whenever R is finite) need to be deduced.
For example, the two rules e . :c -+ :c and (:c . y) . z -+ :c . (y . z) determine
a peak y. Z +-R (e· y). Z -+R e· (y. z), so that the equation y. z ::::: (e· y). z
can be deduced. Since e· (y. z) -+R y. z, the equation can be simplified to
a trivial equation y . z ::::: y . z, which can be deleted.
Orientation of equations into rules is controlled by the given reduction
ordering >- to ensure that only terminating rewrite systems can be derived
from any initial rewrite system contained in >-. For instance, the equation
e- ::::: e can be oriented (with respect to any simplification ordering) into a
rule e- -+ e.
Given an equational inference system I, we write E I-z E' to indicate
that E' can be obtained from E by application of an inference rule of I.

Definition 2.1. A (possibly infinite) sequence Eo I-z El I-z ... is called

a derivation in I from Eo. The (lower) limit U nj~i Ej of a sequence
of equations Eo, E 1 , • •• is denoted by Eoo. Equations in Eoo are called
persisting.
 BASIC COMPLETION 15

An inference system I is said to be sound if, for all sets of equations E

and E', the same equations are provable in E and E' whenever E I- z E'.
Basic completion is sound in this sense.
Lemma 2.2. (Soundness) If E; R 1-6 E'; R', then the congruence rela-
tions +-+EUR and +-+E/UR' are the same.
Proof. Suppose E; R 1-6 E'; R' is by application of an inference rule p.
Evidently, the assertion is true if p is a deduction, orientation, or deletion
inference. If p is a simplification inference, then E = E" U {s ~ t}, E' =
E" U {u ~ t}, and R' = R, where S -+R u. We have S -+R' U +-+E' t and
U +--R s +-+E t, which implies that the two congruence relations +-+EUR and
+-+E/URI are the same. Q.E.D.
If E; R 1-6>- E'; R' and R is contained in the reduction ordering )-,
then R' is also contained in)-. Consequently, the rewrite system Roo is
terminating for any derivation in B>- for which the initial rewrite system
Ro is contained in the reduction ordering )-. Furthermore, the inference
rules of basic completion never decrease the strength of rewriting. That is,
if E; R 1-6 E' ; R' then any term t that is reducible by R is also reducible
by R'.
Definition 2.3. By a basic completion procedure we mean a program that
accepts as input a reduction ordering )- and a set of equations Eo; Ro
where Ro is contained in )-; and uses the inference rules of B>- to generate
a derivation from Eo U Ro. We say that a completion procedure succeeds
for a given input if Eoo = 0 and Roo is convergent. A procedure fails if
Eoo i:- 0. It is called correct if Roo is convergent whenever Eoo =0.
We shall also distinguish between failing and non-failing derivations de-
pending on whether Eoo is empty or non-empty. Correctness requires that
all non-failing derivations result in convergent rewrite systems. We will
present techniques for establishing the correctness, in this sense, of comple-
tion procedures.
If an equational theory can be represented as a convergent rewrite sys-
tem, then equivalence of terms is decidable. Not all equational theories are
decidable in this sense, though. An example of an undecidable equational
theory is combinatory logic:
I·x ~ x
(K·x)·y ~ x
«S·x)·y)·z ~ (x·z)·(y·z)
In general, a completion procedure may either (i) succeed in constructing a
finite convergent system, (ii) fail, or (iii) not terminate and instead compute
successive approximations of an infinite convergent system Roo.
16 STANDARD COMPLETION

2.2. Proof Transformation

We will use binary relations on (equational) proofs to describe the effect of
inferences on the proof level.
Definition 2.4. A (proof) transformation rule is a pair of proofs, writ-
ten P => Q, where P and Q are proofs of the same equation. A (proof)
transformation system is a set of such transformation rules.
For the purpose of transforming proofs we do not distinguish between a
proof P and its inverse p-1.
Definition 2.5. Let n be a proof transformation system. By =>n we
denote the smallest (proof) transformation relation that contains nand
for which p- 1 =>n Q-1, whenever P =>n Q. A proof transformation step
by n is a pair of proofs for which P =>n Q. We also say that P can be
transformed to Q (in zero or more steps) if P =>n
Q.
A transformation system n is called terminating if the corresponding trans-
formation relation =>n is terminating. A proof P is in normal form (with
respect to n) if there is no proof Q such that P =>n Q.
Definition 2.6. A proof transformation system n is said to reflect an
inference system I if E f-z E' implies that every proof P in E can be
transformed by n to some proof pI in E'.
Every basic completion system B is reflected in this sense by a transfor-
mation system ns. For instance, deduction is reflected by transformation
rules of the form

where v )- wand v' )- w'. Orientation, deletion, and simplification are

reflected by transformation rules
where s )- t
where s' )- u '
D
where D denotes the empty proof (i.e., the empty sequence of proof steps),
cf. Figure 2.l.
The proof transformation system n~ (or simply ns if)- is clear from
the context) is the set of all such proof transformation rules. The transfor-
mation relation induced by ns is denoted by =>s.
Lemma 2.7. (Reflection) The proof transformation system ns reflects ba-
sic completion B.
 PROOF TRANSFORMATION 17

• II • t
, ;I
,,
u

/\
,
, ,,
I ,
,,
t ;'
• --------- t • ---------- t u

Figure 2.1: Proof transformation rules

Proof. If E; Rl- s E' ; R' by deduction, then E' =

E U {s ~T t}, R' R, =
and there exists a peak Q of the form s +- R U -+ R t. If P is a proof in
E U R, let P' be the proof in E' U R' obtained from P by replacing each
subproof w[Qu]q by the proof w[su ...... ~Tt tU]q. If P contains no subproof
subproof w[Qu]q, then P = P'. Since each such replacement represents a
proof transformation step by ns, we may conclude that P ~B P'.
Similar arguments apply to the other inference rules. Q.E.D.

Let us illustrate the proof transformation process with the axioms of

group theory:

e·x ~ x

(x· y) . z ~ x· (y. z).

The equation x-- . e ~ x is provable:

x ·e ...... E x-- . (x- . x)

...... E (x-- . x-)· x
...... E e· x
...... E X.

Let now 'rlpo be the lexicographic path ordering corresponding to a prece-

dence 'r in which· 'r - 'r e. By repeated orientation of equations we obtain
the following rewrite system R 1 :

(x . y) . z -+ x· (y . z).
18 STANDARD COMPLETION

These inference steps are reHected by a sequence of proof transformation

steps Po =>~ Pl , where Po is the above proof and Pl is

The middle two steps of this proof form a peak which is an instance of a
more general peak
x- . (x . y) +-R 1 (x- . x) . Y - R1 e .Y

involving the third and second rule of R l . We can deduce the equation
x- . (x . y) ~ e . y and obtain a new proof P2 :
x-- . (x- . x) +-+E2 e.x

where E2 consists of the new equation and R2 =

R l . Again we have
Pl =>~ P2 • The equation x- ·(x·y) ~ e·y can be simplified to x- ·(x.y) ~ y
and then oriented. This is reHected by a proof transformation P2 =>~ Pa,
where P a is
e· x
- R3 X +-R3 - R3 x.
The "trivial" peak x +-R3 e.x - R3 x can be simplified away, so that we
obtain a proof

- R3 x.

The initial equation x-- . e ~ x can now be deduced immediately (and

then oriented). The set of all derived rules
e ·X
x-
-- x

--
·X e
(x· y) . z x . (y . z)

-
x- . (x· y) y
x ·e x
is not convergent, however. For instance, the equation e-·y ~ y is provable,
but not by a rewrite proof. If we continue the completion process (and
intersperse it with additional simplification rules) a convergent system of
ten rules can be obtained eventually:
 PROOF SIMPLIFICATION 19

e· z --+ z z·e --+ z

z - ·z --+ e z·z- --+ e
(z . y) . z --+ z· (y. z) z -- --+ z
e --+ e (z· y)- --+ y- ·z -
z- . (z· y) --+ y z· (z- . y) --+ .y

(Knuth and Bendix 1970).

2.3. Proof Simplification

Each proof transformation step by 'R8 decreases the complexity of a proof
with respect to some well-founded measure. Consequently, there are no
infinite proof transformation sequences.

Lemma 2.8. The proof transformation system 'R8 is terminating.

Proof. We define a measure of the complexity of a proof by assigning a

certain cost to each proof step. The cost of a proof step s +-+~I':ITti t is the
multiset {s,t}; the cost of a proof step s +-+~I':I.1.tI t is the multiset {s}, if
u >- v, and {t}, if v >- u. The complexity of a proof is the multiset of all
costs of its proof steps. (Note that a proof P has the same complexity as
the inverse proof p-l.)
For example, the proof

has complexity

We define an ordering >-8 on proofs by comparing proofs according to

their complexity, using the twofold multiset extension (>-mul)mul of the
given reduction ordering >-. The ordering >-8 is a proof reduction order-
ing and contains the transformation system 'R8. As a consequence, the
transformation relation :::}~ is well-founded. In detail:
i) Orientation. We have s +-+:I':ITt t >-8 s --+:I':I.1.t t, because {s, t} >-mul
{s}.
ii) Simplification. We have s +-+~Tt t >-8 s --+~'I':I.1.U' u +-+~I':ITt t, because
s>- u and therefore {s,t} >-mul {s} and {s,t} >-mul {u,t}.
iii) Deletion. Trivially, s +-+:I':IT4 s >-8 0
iv) Deduction. We have s -~I':I.1.tI u --+!'I':I.1. W' t >-8 s +-+:I':ITt t; because
{u} >-mul {s,t}. Q.E.D.
20 STANDARD COMPLETION

Let Eo; Ro t- B E 1 ; Rl t- B .•. be a derivation in 8. Since the proof

transformation system 'RB is terminating and reflects the inference system
B, every proof Pi in Ei U R; can be transformed by 'RB to a normal-form
proof in Eoo U Roo. To prove correctness of completion it suffices to show
that these normal-form proofs are rewrite proofs. In other words, com-
pletion can be interpreted as a process of proof normalization, the goal of
which is the derivation of rewrite proofs.

2.4. Fairness and Correctness

A large class of correct completion procedures can be characterized via the
following notion of fairness.

Definition 2.9. Let N be a set of proofs, 'R be a proof transformation

system, and I be an inference system. A derivation Eo t-z El t-z ... is said
to be fair with respect to N and'R if for every proof P in Eoo that is not
contained in N, there exists some proof Q in Ui Ei, such that P Q.::}:k
Theorem 2.10. Suppose 'R is a terminating proof transformation system
and reflects the inference system I. If a derivation Eo t-z El t-z ... is fair
with respect to Nand 'R, then every proof P in Ui Ei can be transformed
by'R to a proof in N.

Proof. Suppose some proof in Ui Ei cannot be transformed to a proof in

N. Let P be a minimal such proof with respect to the well-founded ordering
::}:k.Since any proof in Ui Ei can be transformed to a proof in E oo , we
may infer that P is a proof in Eoo. Since P is not contained in N, we may
use fairness to infer that there exists a proof Q in U Ei with P Q. ::}:k
This contradicts the assumption that P is in normal form with respect to
'R. Q.E.D.

Let N'; (or N B ) be the set of all rewrite proofs s ~:R u +-:R t, where
R denotes any rewrite system contained in >-. We shall derive sufficient
conditions for the fairness (with respect to NB and 'RB) of derivations in
basic completion.
A proof in R is a rewrite proof if and only if it contains no peak s +- R
U ~R t. In other words, fairness (in the case of basic completion) requires
elimination of peaks. First observe that a peak can always be transformed
to a rewrite proof, provided a rewrite proof exists.

Lemma 2.11. If P is a peak 8 +-R u ~R t and Q 18 a rewrite proof

8~:R v +-:R t, then P::}~ Q.
 FAIRNESS AND CORRECTNESS 21

Proof. Transform the peak s -R U -R t into an equality step s +-+E t and

then repeatedly simplify to obtain a proof s -:R v +-+E v -:R t from which
the equality step can be deleted. The result is a rewrite proof s -:R v -:R t
in R. Q.E.D.
If S - R U - R t is a peak, but there exists no rewrite proof of s ~ t in
R, then new equations need to be deduced with which a rewrite proof can
possibly be constructed. Certain equational consequences called "critical
pairs" are of importance in this regard.
Definition 2.12. Let s ~ t and u ~ v be equations with no variables
in common (if necessary the variables of one equation are renamed) and
suppose that some non-variable subterm sip of s is unifiable with u, u
being the most general unifier. Then the superposition of u ~ v on s ~ t
at position p determines a critical pair tu ~ su[vu]p. The proof tu -;~.
su -~~V su[vu]p is called a critical overlap; the term SU, the overlapped
term; the position p, the critical pair position.
For example, superposing the equation x . x- ~ e on (x· y)- ~ y- . x-
yields a critical pair x-- . x- ~ e-. The corresponding critical overlap is
x-- ·X- - E (x·x-)- - E e-.
Critical pairs t ~ t are called trivial. (For instance, critical pairs ob-
tained by superposing an equation on literally the same equation at the
topmost position p = A are trivial.) By CP(E) we denote the set of all
non-trivial critical pairs between equations in E. The set CP(E) is finite
whenever E is finite. Observe that usually CP(E) # CP(E- 1 ).
Lemma 2.13. (Critical Pair Lemma, Knuth and Bendix 1970) If P is a
peak S - E U - E t, then either there exists a rewrite proof S -:E v -:E t
or a "critical-pair proof" S +-+CP(E) t.
Proof. Let E be a set of equations {v ~ w, v' ~ w'} and P be a peak
S -!:,~v U -:f~Wf t in E. If S = t, then the empty proof is a suitable
rewrite proof of S ~ t. Let us therefore assume that sand t are distinct.
Let u and u' be substitutions such that ul p = vu, ul q = v'u', S = u[wu]p,
and t = u[ w' u']q. We distinguish three types of peaks, called non-overlaps,
variable overlaps, and proper overlaps, respectively.
If the two positions p and q are disjoint, we speak of a non-overlap.
Then slq = (u[wu]p)lq = ulq = v'u' and tip = (u[w'u']q)lp = ul p = vu,
so that there exists a rewrite proof s -:f~Wf u[wu, w' u']p,q -!:,~v t (see
Figure 2.2).
For example, since the two rules x . x- - e and e . x - x are applied
at disjoint positions in
22 STANDARD COMPLETION

Figure 2.2.: Non-overlap

the peak can be replaced by a rewrite proof

e· (e· x) -+R e.x +-R (x· x-)· x.

If P and q are not disjoint, one position has to be below the other. Let
us assume, without loss of generality, that q is below P and let p' be a
=
position such that q pp'. Then vulpl (ulp)lpl = = =
ulppl ulq v'u'. If p'=
is a position in v and vlpl is not a variable, we speak of a proper overlap.
Otherwise, we speak of a variable overlap (or say that one proof step applies
in the "variable part" of the other).
In other words, if P is a variable overlap, then there exist positions
q' and q", such that p' = q' q" and v Iql =
x, for some variable x, and
vulpl = VUl q1 qll = (vulql)lqll = xul qll =
v'u'. Define the substitution T
so that XT = xu[w' U']qll and yr
II
= yO', for all variables y different from
x. Since xu -+!/R.lWI XT, there exists a proof sip = WU -+EI WT, where
E' = {v' R:j w'}. Let now Pl, ... ,Pn be all those (pairwise disjoint) po-
sitions in v at which the variable x occurs. Since tip =
(u[w'u']q)lp =
(u[w'u']ppl)lp = ulp[w'u']pl = vu[W'U']pl =
vU[XT]ql and q' is one of the
positions Pi, there is a proof tip -+EI VU[XT, ... , XT]Pl •...•P.. =
VT. In sum,
we have s = u[wu]p -+EI U[WT]p and t -+EI U[VT]p. Since E' ~ E, we
may conclude that there exists a rewrite proof s -+E S' +-E t' +-E t (cf.
Figure 2.3).
Suppose, for example, that R contains the rules X·X- -+ e and e·x -+ x.
The variable overlap

e +-R (e . x) . (e . x)- -+R x . (e . x)-

 FAIRNESS AND CORRECTNESS 23

, ,

.~~-- ~
Figure 2.3: Variable overlap

can be replaced by a rewrite proof

Finally, suppose P is a proper overlap. Let us assume without loss of

generality that v ~ wand Vi ~ Wi have no variables in common. (If the
two equations do have variables in common, consider the peak s -~:::;:v
U -+!I1:::;:WIl t instead, where v" ~ w" is literally similar to Vi ~ Wi, but has
no variables in common with v ~ w.) Since (v Ipl)u = VU Ipl = Vi u' , the
two terms vlp and Vi are unifiable. Let r be a most general unifier and let
l

r' be a substitution, such that (xr)r' = xu, for all variables x occurring
in v ~ w or Vi ~ Wi. Then P = u[Qr']p, where Q is the critical overlap
,\ pi
wr -w:::;:v vr -+VI:::;:WI vr[w'r]pl. Q.E.D.

Note that the proper-overlap case can be characterized more precisely:

Corollary 2.14. If P is a proper overlap s -~:::;:v U -+!,:::;:w, t, where v ~ w

and Vi ~ Wi have no variables in common, then P can be written as u[Qr]r,
for some term u, position r in u, substitution r, and critical overlap Q.

The Critical Pair Lemma suggests the following sufficient condition for
fairness.
24 STANDARD COMPLETION

Lemma 2.15. A non-failing derivation Eo j Ro rs El j Rl rs ... in basic

completion is fair (with respect to Hs and"Rs) if the set of critical pairs
CP(Roo) is a subset of the set Ut Et of all deduced equations.

Proof. Let Eo j Ro rs El j Rl rs ... be a derivation for which Eoo = 0

and CP(Roo) is a subset of Ut Et. It suffices to prove that for every peak
P of the form s +-Roo U --+Roo t, there exists a proof Q in Ut(Et U Rt),
such that P::}~ Q.
If there exists a rewrite proof s --+Roo v +-Roo t, we may use Lemma 2.11
to infer that P ::}~ Q, for some proof Q in Roo. If there exists no such
rewrite proof, then by the Critical Pair Lemma (and Corollary 2.14) P =
W[P'T']p, for some term w, position p in w, substitution T', and critical
overlap P'. But then s +-+CP(Roo) t so that by fairness s +-+E; t, for some
j ~ o. This implies that there is a suitable proof Q with P ::}~ Q. Q.E.D.

Usually, a completion procedure is called fair if it generates only derivations

for which all critical pairs between persisting rules are computed. 1
Applying Theorem 2.10 to basic completion we obtain:

Proposition 2.16. (Correctness) If a non-failing derivation in basic com-

pletion is fair, then the limit rewrite system Roo is convergent.

Proof. Lemmas 2.7, 2.8, and 2.15 show that Theorem 2.10 can be applied
to the basic completion system B>- , the set of proofs Hs , and the transfor-
mation system "Rs. Consider a non-failing derivation in basic completion.
The limit rewrite system Roo is contained in >- and hence is terminating.
=
Since the derivation does not fail, we have Eoo 0. Also, by Theorem 2.10
every proof P in Roo can be transformed to a rewrite proof, which implies
that Roo is Church-Rosser. In sum, Roo is convergent. Q.E.D.

The well-known characterization of the Church-Rosser property of ter-

minating rewrite systems in terms of critical pairs can also be easily proved
via proof orderings.

Definition 2.17. A rewrite system R is convergent on a set of equations

E if every equation s ~ t in E is provable by a rewrite proof s --+R v +-R t.

Proposition 2.18. A terminating rewrite system R is Church-Rosser if

and only if it is convergent on the set of critical pairs CP(R).
1 Dershowitz (1989) insists on a stronger fairness condition which requires a procedure
to produce a fair derivation whenever one exists. Fairness in this stronger sense may
require the enumeration of all possible derivations from a given initial set Eo u Ro.
 STANDARD COMPLETION 25

Proof. The only-if direction is obvious. For the other direction, let ~
be the reduction ordering --+k (note that R is terminating) and ~13 be the
corresponding proof ordering. We claim that whenever P is a minimal proof
(with respect to ~ 13) of an equation s ~ t in R, then it is a rewrite proof.
For if P is not a rewrite proof, it must contain a peak s' +- R U' --+ R t'.
But then we may use the Critical Pair Lemma in combination with the
fact that R is convergent on CP(R), to infer that there is a rewrite proof
s' --+R v' +-R t', which contradicts the minimality of P. In sum, if an
equation is provable, then it is provable by a rewrite proof. This implies
that R is Church-Rosser. Q.E.D.

A rewrite system R is said to be non-overlapping if no left-hand side

s of a rule in R is unifiable with any term that is literally similar to a
non-variable sub term of some other left-hand side or a proper non-variable
subterm of s. If R is non-overlapping, then CP(R) = 0. Non-overlapping,
terminating systems are therefore convergent.
Typical examples of non-overlapping systems are many equational pro-
grams, such as the following rewrite system for symbolic differentiation
("with respect to X"):

D(X) --+ 1
D(Y) --+ 0
D(-x) --+ -D(x)
D(x + y) --+ D(x) + D(y)
D(x x y) --+ D(x) x y+x x D(y)
D(x -7Y) --+ D(x) -7 Y - (x x D(y» -7 (y2)
D{lnx) --+ D(x) -7X
D(xY) --+ D(x) x (y x x y - 1 ) + ({lnx) x D(y» x (xY)

(Knuth 1973, p. 337). This rewrite system is non-overlapping and termi-

nating; hence convergent. (Termination can be proved by a recursive path
ordering with a total precedence in which D is maximal.)
Having outlined our approach by using the basic concepts of inference
systems, proof orderings, and normal-form proofs to prove the correctness of
basic completion, we shall proceed with a discussion of more sophisticated
completion methods.

2.5. Standard Completion

Basic completion consists of fundamental inference rules commonly used
in constructing convergent systems. For efficiency reasons additional fea-
tures, such as more extensive simplification, are indispensable in practice.
26 STANDARD COMPLETION

The following inference rules suffice to formulate such simplification mech-

amsms:
E;RU{s-t}
COMPOSITION: ift -R u
E;RU{s-u}

E;RU{s-t}
COLLAPSE: if there is a proof s -~~.l.W u
EU{uRlt};R in R, where s t> v

The symbol t> denotes the strict part of the encompassment ordering,2
which is defined as follows: s ~ t if some subterm of s is an instance of t,
but not vice versa. For example, x + (x + 0) t> x + y.
By a standard completion system we mean any inference system C>-
consisting of B>- plus the inference rules above.
Composition allows simplification of right-hand sides of rewrite rules;
collapse, of left-hand sides. While composition produces another rewrite
rule, the equation obtained by collapsing a rule need not necessarily be
orient able with respect to the given reduction ordering~. Note that a
rewrite rule must not be used to collapse another rewrite rule with a literally
similar left-hand side. This restriction is of no relevance in practice, for if
equations are always fully simplified before they are oriented (as is the case
in most implementations of completion), then no two rules with literally
similar left-hand sides can be produced. In such procedures the collapse
rule can be applied without explicitly checking whether the condition s t> v
is satisfied.
Inference systems C>- are evidently sound, in that the congruence rela-
tions ...... EUR and ......E'UR' are the same whenever E; R I-c E'; R'. Also, if
E ; R I-c E' ; R' and the reduction ordering ~ contains R, then ~ also con-
tains R'. Consequently, the system Reo is terminating for any derivation
for which the initial rewrite system Ro is contained in the reduction or-
dering ~. As with basic completion, the inference rules never decrease the
strength of rewriting: if E; R I-c E'; R' then any term t that is reducible
by R is also reducible by R'.
Collapse and composition are reflected by proof transformation rules of
the form

S -;~.l.t t
S -;~.l.t t
where s ~ t, s ~ u, t' ~ u', v ~ w, and s t> v (see Figure 2.4).
2The collapse rule can be defined in terms of an arbitrary well-founded ordering, but
virtually all implementations of completion are based on the encompassment ordering.
 STANDARD COMPLETION 27

• ~ t
, , If
, ,,
,,
I , "
t )t'
u u

Figure 2.4: Transformation rules for standard completion

We denote by 'R~ (or simply 1lc) the set consisting of 'R~ plus all these
transformation rules. The corresponding transformation relation is denoted
by =>c.
With these definitions we have:
Lemma 2.19. The proof transformation system 'Rc reflects the standard
completion system C.
Lemma 2.20. The transformation system 'Rc is terminating.
Proof. We redefine the cost assigned to single proof steps to accommodate
composition and collapse. The cost of a proof step s ....~~TV t is the quadru-
ple ({ s, t},.1,.1, .i); the cost of a proof step s ....~~.J..v t is the quadruple
({s},slp,u,t), ifu >- v, and ({t},tlp,v,s), if v >- u. Again, the complexity
of a proof is the multiset of all costs of its proof steps. (Thus a proof P has
the same complexity as the inverse proof P- 1 .)
Proof steps are compared according to their complexity using the lexi-
cographic combination >-c of the multiset extension >-mul of the reduction
ordering >-, the subterm ordering, the encompassment ordering J2>, and the
reduction ordering >-. To compare proofs we use the multiset extension of
this ordering. The corresponding ordering >-c is a proof reduction ordering
and contains the proof transformation system 'Rc. This can easily be veri-
fied for the proof transformation rules of 'RB, using the same arguments as
in Lemma 2.8. In the remaining cases we have:
i) Composition. We have s -?;~.J..t t >-c S -?;~.J..u U +-~/~.J..t' t, as s >- t
and t' >- u' imply
{( {s }, s, s, t)} >-c {({s }, s, s, u), ({t}, tip, t', u)}.
ii) Collapse. Since s >- t, s>- u, and s I> s', we have
{({s},s,s,t)} >-c {({s},slq,v,u),({t,u},.1,.1,.1)},
Q.E.D.
28 STANDARD COMPLETION

The following theorem is an immediate corollary of Theorem 2.10:

Theorem 2.21. If a non-failing derivation by standard completion proce-

dure is fair (with respect to.!VB and'R.c), then the limit rewrite system Roo
is convergent.

It can easily be shown that a derivation is fair if all critical pairs between
persisting rules are computed, i.e., if CP(Roo) is a subset of Uk Ek. For
the purpose of establishing the correctness of most practical completion
procedures the following stronger result is essential.

Proposition 2.22. A non-failing derivation Eo ; Ro I-c E 1 ; Rl I-c ... is

fair (with respect to.!VB and 'R.c) if for every critical overlap P of the form
s +-Roo U -Roo t there exists a proofQ of s ~ t in Us(Ei URi), such that
P >-c Q.

Proof. We will prove that every proof of 8 ~ t in Ui(Ei U Ri) can be

transformed by 'R.c to a rewrite proof in Roo. Suppose some proof cannot
be transformed to a rewrite proof in Roo. Let P be one such proof that is
minimal with respect to the proof ordering >-c.
Since every proof can be transformed by 'R.c to a proof in Eoo U Roo
and Eoo = 0, we may infer that P is a proof in Roo, but contains a peak
8' +-Roo U' -Roo t'. If this peak is not a proper overlap, then there exists a
rewrite proof 8' -Roo v' +-Roo t' and we may use Lemma 2.11 to infer that
there is a proof Q such that P ~t Q. Since P >-c Q, the proof Q can be
transformed to a rewrite proof in Roo, which is a contradiction.
If the peak is a proper overlap, then it can be written as u[Q"u]p, where
Q" is a critical overlap between rules in Roo. By assumption there is a proof
Q' of 8' ~ t' such that Q" >-c Q', and consequently u[Q" u]p >-c u[Q' u]p.
Since P >-c u[Q'u]p, the proof u[Q'u]p can be transformed to a rewrite
proof 8' -Roo v' +-Roo t'. But then there is a proof Q such that P ~t Q,
which is a contradiction. Q.E.D.

The notion of completion, as we have formalized it above, covers a

wide variety of specific completion procedures, including the procedures
described by Huet (1981) and Dershowitz (1982b). The latter procedure is
described below. It accepts as input a set of equations Eo and a reduction
ordering >-.
Let E be Eo and R be the empty set. Then repeat as long as
equations are left in E. If none remain, terminate successfully.
1. Remove an equation 8 ~ t (or t ~ 8) from E such that
8>- t. If none exists, terminate with failure.
 STANDARD COMPLETION 29

2. Add the rule s - t to R.

3. Use R to reduce the right-hand sides of existing rules.
4. Add to E all critical pairs formed using the new rule.
5. (Optional) Remove all old rules from R whose left-hand
side contains an instance of s.
6. Use R to reduce both sides of equations in E to normal
forms. Remove any equation whose reduced sides are iden-
tical.

This procedure is a standard completion procedure. Step 2 represents

an application of orientation; step 3, repeated application of composition;
step 4, repeated deduction; step 6, repeated simplification and deletion.
Step 4, in combination with step 5, implicitly uses collapse. For whenever
a rule s - t can be collapsed to u ~ t, then u ~ t is a critical pair in
CP(R). In the above procedure, the equation u ~ t is first deduced in
step 4, but may be deleted in step 5.
Observe that equations in E are kept in fully simplified form (step 6).
Consequently, whenever an equation s ~ t is selected in step 1, then both
sand t are irreducible with respect to the current rewrite system R. This
guarantees that R will never contain two rules with literally similar left-
hand sides, so that the condition for applying collapse inferences is always
satisfied.
The above procedure may generate critical pairs from non-persisting
rules that are not necessary. On the other hand, not all critical pairs
between persisting rules are generated either. For if the right-hand side of
a rewrite rule is simplified, in step 3, no critical pairs are computed with
the new simplified rule. Nonetheless, according to Proposition 2.22 the
procedure is correct.
More precisely, suppose there is a proof t -R t' and some rule s - t
in R is replaced by s - t' as a result of composition. Then for every
critical overlap P involving the new rule s - t', there exists a proof Q with
P >-c Q. Suppose P is a critical overlap vu +-~I::lU uu[su]p -~I::l" uu[t'u]p.
Since the critical pair vu ~ uu[tu]p, which is obtained from the overlap
vu +-~I::lU uu[su]p -~I::lt uu[tu]p, has already been computed, there exists
a proof Q = vu +-+!Ul::luu[,u]p uu[tu]p +- R uu[t' 0'] in which all terms are
strictly smaller than UO'. As a consequence, we have P >-c Q. A similar
argument applies to critical overlaps t' 0' +-t'1::l3 sO'[uO']p -~l::ltJ su[vO']p.
The extensive use of simplification, composition, and collapse is typical
of completion procedures.

Definition 2.23. A derivation is called simplifying if Roo is a reduced

30 STANDARD COMPLETION

rewrite system and all equations in Eoo are unorientable with respect to >-,
yet irreducible by Roo.
In other words, if a derivation is simplifying then all persisting equations
are fully simplified and the persisting rules form a reduced rewrite system.
Most implementations of standard completion procedures are simplifying
in this sense: they construct reduced convergent rewrite systems, whenever
they succeed.
Implementations of standard completion have been described, among
others, by Lescanne (1983) and Kapur and Sivakumar (1984). Lescanne
(1989) describes an implementation of completion that is directly based on
inference rules (and a suitable control).
Completion has been applied to a variety of problems including the word
problem in universal and finitely presented algebras (Knuth and Bendix
1970, Le Chenadec 1986) and equational programming (Dershowitz 1985).
A number of convergent system have been derived with such procedures.
The following examples are from Knuth and Bendix (1970).
Example 2.24. The theory of a single axiom z- . (z . y) ~ y, expressing a
property of the inverse operator, can be represented as a convergent system
of three rules:
z . (z· y) -+ y
z .y -+ z·y
z . (z- . y) -+ y
Example 2.25. Central groupoids are also characterized by a single axiom
(z . y) . (y. z) ~ y and can be represented as a convergent system of three
rules:
(z . y) . (y . z) -+ y
z . «z . y) . z) -+ z· Y
(z . (y . z» . z) -+ y. z
Example 2.26. Algebraic systems with a left identity and a right inverse
are called left groups:

~ e
z . (y . z)
A convergent rewrite system for this theory is:
e·z -+ z e -+ e
z·z -+ e z·e -+ z--
(z . y) . z -+ z . (y . z) z .y -+ z·y
z· (z- . y) -+ y z- . (z· y) -+ y
z -+ z (z· y)- -+ y - ·z-
 CRITICAL PAIR CRITERIA 31

The correctness of a specific completion procedure was first proved by

Huet (1981). An advantage offormulating completion as an equational in-
ference system is that correctness can be proved for a wide class of different
completion procedures. The proof ordering approach is comparatively sim-
ple and intuitive, especially for dealing with simplification inferences. The
intrinsic difficulty of applying the approach consists in finding a suitable
ordering to establish proof normalization. Once an appropriate proof or-
dering has been found, the remaining verification steps are straightforward.
Various minor improvements of standard completion can readily be ver-
ified in the proof ordering framework. For instance, since fairness requires
only computation of critical pairs between persisting rules, critical pairs
that originated from a collapsed rule can be deleted (provided, of course,
that they have not yet been used for simplification). Furthermore, an in-
ference rule,
E U {s ~ t, u[sO']p ~ u[tO']p}; R
SUBSUMPTION:
EU{s~t};R

can be added to standard completion without impairing correctness. "Ori-

entable instances" of equations can be used for simplification. That is, if
u ~ v is an equation and UO' >- VO', then the rewrite rule UO' -+ VO' can be
used for simplification (see Chapter 4).
Inference rules can also be formulated in terms of a proof ordering. For
example,
EU{s~t};R
DELETION: if S ~;Rlt t >-c P, for
E;R some proof P in E U R
is a generalized version of the deletion inference rule. The inference rules
for simplification of rewrite rules, composition and collapse, can be gener-
alized in a similar way. Further details can be found in Chapter 4. Similar
inference rules have turned out to be particularly useful in the context of
conditional completion procedures (Ganzinger 1987).

2.6. Critical Pair Criteria

The efficiency of the completion process depends primarily on the number
of critical pairs that are generated. Simplification can be very effective in
eliminating superfluous equations. For instance, any critical pair s ~ t for
which both sand t can be reduced to a common normal form, is redundant.
But systematic normalization of terms can be costly, while the redundancy
of a critical pair can often be determined more efficiently by examining the
structure of the associated critical overlap.
32 STANDARD COMPLETION

Definition 2.27. A critical pair criterion is a mapping CPC on sets of

(labelled) equations, such that CPC(E) ~ CP(E).

Critical pairs in CPC(E) are meant to be redundant.

Definition 2.28. A critical pair criterion C PC is said to be sound if, for

all terminating rewrite systems R, whenever R is convergent on CP(R) \
CPC(R), then it is convergent.

In other words, a sound criterion provides a characterization of the Church-

Rosser property. To be of use in practice, a criterion also has to be com-
patible with the simplification mechanisms employed by completion.

Definition 2.29. A derivation Eo; Ro I-c El ; Rl I-c ... in standard com-

pletion is said to be fair with respect to a critical pair criterion C PC
if for every critical overlap P associated with a critical pair S R:: t in
CP(Roo) \ U CPC(Ei URi) there exists a proof Q of s R:: tin Ui(Ei URi),
such that P >-c Q. A criterion CPC is correct if every non-failing deriva-
tion that is fair with respect to C PC is also fair with respect to 'Rc and
Ns.

Evidently, if a non-failing derivation is fair with respect to a correct cri-

terion C PC, then Roo is canonical. The following lemma follows from
Proposition 2.22.

Lemma 2.30. A critical pair criterion CPC is correct if for every set of
equations E and every critical overlap P associated with a critical pair s R:: t
in C PC(E) there exists a proof Q of s R:: t in E, such that P >-c Q.

Proposition 2.31. Any correct critical pair criterion is sound.

Proof. Let CPC be a correct criterion, R be a terminating rewrite system,

and >- be the reduction ordering induced by R. Furthermore, suppose R
is convergent on CP(R) \ CPC(R). We have to show that R is Church-
Rosser. The (one-step) non-failing derivation 0; R is fair with respect to
CPC. By the correctness of CPC it is also fair with respect to Ns and
'Rc. By Theorem 2.21 the rewrite system R is Church-Rosser. Q.E.D.

A sound criterion need not necessarily be correct. For instance, Zhang

and Kapur (1989) suggest a criterion PCP for standard completion, where
PC P( E U R) consists of all critical pairs of a rule u --+ v in R on another
rule s --+ t in R at a position pq, such that p i= A i= q and the overlapped
 CRITICAL PAIR CRITERIA 33

term StT is reducible at position p. This criterion can be shown to be sound

without much difficulty, but is not correct.3 For instance, the derivation

0; {h(a) -+ a, f(g(x, h(x))) -+ a, g(a, h(a)) -+ a}

I-c {g(a, a) ~ a}; {h(a) -+ a,/(g(x, h(x))) -+ a}
I-c 0; {h(a) -+ a,/(g(x, h(x))) -+ a, g(a, a) -+ a}
is fair with respect to PCP. The only critical pair between the final three
rules is a ~ f(g(a,a)), which is obtained by superposition of h(a) -+ a on
f(g(x, h(x))) -+ a. This critical pair is in PCP(Eo U Ro) and therefore is
superfluous according to the criterion. But even though the above deriva-
tion is fair with respect to PCP, the final rewrite system is not convergent,
as the term f(g(a,h(a))) has two different normal forms f(a) and a.
An example of a correct criterion is blocking, a concept introduced by
Slagle (1974) and applied to rewriting by Lankford and Ballantyne (1979).

Definition 2.32. Let E be a set of equations and ttT +-~. StT -+~~tJ
StT[VtT]p be a critical overlap in E. The overlap is said to be non-blocked
(with respect to >-) if there exist a term wand a variable x in s or u, such
that XtT -+E W and XtT >- w. Otherwise, it is called blocked.

A critical pair is blocked if the corresponding critical overlap is blocked.

The set BCP(E) consists of all non-blocked critical pairs in CP(E).

Proposition 2.33. The non-blocked criterion BCP is C01Tect.

Proof. If ttT ~ StT[VtT]p is a non-blocked critical pair, then XtT -+E w,

where XtT >- wand x occurs in s or u. Let tT' be the substitution for which
XtT' = w and ytT' = ytT, for all variables y distinct from x. Let Q be the
proof ttT -+8 ttT' +-E StT' -+E StT'[VtT']p +-8 StT[VtT]p (see Figure 2.5). Then
P >-c Q and we may use Lemma 2.30 to infer that the criterion BCP is
correct. Q.E.D.

The proposition shows that non-blocked critical pairs may be ignored

by completion. The non-blocked criterion BCP is a special case of the
following connectedness criterion.
Definition 2;34. Let E be a set of equations. Two terms sand t are
said to be connected below U in E (with respect to >-) if there are terms
Ul. ••. , Un, such that s +-+E Ul +-+E ••• +-+E Un +-+E t and U >- Ui, for all i
with 1 ~ i ~ n.
3Zhang and Kapur attribute the criterion to Winkler and Buchberger (1983), but
the latters' actual, more subtle criterion is a specific instance of the composite criterion
described below, and is correct.
34 STANDARD COMPLETION

..----
to'
I
.00[uO']1'
---... .O'[VO']1'
I
I I
I .0' I
1 _-- ...... 1
T ........... .....-... ,
to'

Figure 2.5: Non-blocked overlap

Connectedness was introduced by Buchberger (1984). The inference rules

of standard completion preserve connectedness. That is, whenever E; R f-c
E' ; R' and two terms sand t are connected below u in E U R, then they
are also connected below u in E' U R'. The concept can readily be utilized
for a critical pair criterion, as we may view completion as a process of
establishing, for every critical overlap s +-R u - R t, the connectedness
of sand t below the overlapped term u. For instance, adding the critical
pair s ~ t as a new equation is one way of establishing connectedness.
Conversely, if sand t are already connected, then the critical pair s ~ t is
superfluous.
We define CCP(E) as the set of all critical pairs s ~ tin CP(E) such
that sand t are connected below the associated overlapped term u.
Proposition 2.35. The connected critical pair criterion CCP is correct.

Proof. Observe that if P is a critical overlap of the form s +-R u - R t,

where sand t are connected below the overlapped term u, then there exists
a proof Q of s ~ t, such that P >-c Q. Q.E.D.

A criterion based on connectedness was first formulated by Buchberger

(1979) for a completion-like algorithm for constructing canonical bases for
polynomial ideals. Various criteria for standard completion, based on con-
nectedness with respect to the reduction ordering -~ induced by R, have
been developed by Winkler and Buchberger (1983), Winkler (1985), and
Kiichlin (1985, 1986b). These criteria differ in the respective tests used to
ensure connectedness. Let us sketch the basic idea.
Suppose s +- R U - R t is a critical overlap and u can be rewritten to
some term v by R. We can decompose the original overlap into two peaks
s +-R U - R v and v +-R U - R t. If S +-R U - R V is a non-overlap or
a variable overlap, then s and v are connected below u. Otherwise, the
equation s ~ v can be written as u'[s'u]p ~ u'[v'u]p, for some critical pair
 CRlTICAL PAIR CRITERIA 35

s' ~ v'. If this critical pair has already been computed, then s and v are also
connected below u. Similar arguments apply to v and t. Connectedness can
therefore often be verified by checking whether certain critical pairs have
already been computed. Book-keeping mechanisms to that end have been
proposed by Kiichlin (1985, 1986b) and Winkler (1985).4
For instance, suppose that all rewrite rules are numbered during com-
pletion in such a way that no two rules in any system Rn are assigned the
same number. In addition, a rule is marked once all critical pairs with
lower-numbered rules have been computed. Let P be a critical overlap as
described above and suppose the rules numbered i, j, and k, respectively,
are applied in the proof steps u -+R S, U -+R t, and U -+R v. If rule
max(i, k) is marked, then all critical pairs between the corresponding rules
have been computed, so that s and v are connected below u. Similarly, if
rule max(j, k) is marked, then tand v are connected below u.
The emphasis in the papers cited above is on soundness and practical-
ity, though Winkler (1985) and Kiichlin (1986b) also prove the correctness
of specific versions of completion that incorporate tests for connectedness.
Winkler's proof is similar to the proof of correctness of standard comple-
tion in Huet (1981); Kiichlin's proof is based on multiset induction. Harald
Ganzinger [personal communication] has pointed out that connectedness
criteria are implicitly used in most completion procedures, e.g., in the pro-
cedures described by Huet (1981) and Dershowitz (1982b).
Connectedness is essentially a concept based on terms. A similar idea
can be applied to equational proofs, which motivates the following defini-
tion.

Definition 2.36. A peak s +-E U -+E t is said to be composite in E (with

respect to the proof ordering >-c) if there are proofs Pi, ... , Pn in E, where
Pi is a proof of Ui-i ~ Ui, such that Uo = s, Un+i = t, U >- Ui, and
(s +- E U -+ E t) >-c Pi. The proof Pi ... Pn is called a decomposition of the
peak s +-E U -+E t.

A critical pair s ~ t is composite if its corresponding critical overlap is

composite. By PCP (E) we denote the set of all composite critical pairs of
E.

Proposition 2.37. The composite criterion PCP is correct.

Proof. Let Eo; Ro rc E i ; Ri rc ... be a derivation that is fair with

respect to PCP and for which Eoo = 0. We prove by induction on >-c that
'The test described by Winkler restricts the position at which the rewrite step u -- R v
may apply, whereas no such restriction is imposed by Kiichlin.
36 STANDARD COMPLETION

every proof Pin Ui(Ei U~) can be transformed by ::}l

to a rewrite proof
in Roo. The assertion is assumed to be true for all proofs Q with P >-c Q.
If P is not a proof in Roo or contains a non-proper overlap, then there is
l
some proof Q, such that P ::} Q. Suppose P is a proof in Roo, but contains
a proper overlap S +-Ri U -+Ri t. This proper overlap can be written as
u[P'u]p, where P' is a critical overlap. Let s' ~ t' be the corresponding
critical pair in CP(Roo). If the critical pair s' ~ t' is contained in some
set E,,, then there is some proof Q in U(Ei U ~), such that P ::}l
Q.
If the critical pair is not contained in any set Eli:, then by fairness it has
to be contained in some set PCP(Ej,Rj), which implies that there is a
decomposition Pl , ... , Pn of u[P'u]p. Since P !:c u[P'u]p >-c Pi, for all i
with 1 ~ i ~ n, we may use the induction hypothesis to infer that each
proof Pi can be transformed to a rewrite proof Qi in Roo. Let Q' be the
composition Ql ... Qn of all these rewrite proofs. Since all terms in Q'
are strictly smaller than u, we have P >-c Q and may apply the induction
hypothesis again, to conclude that there is a rewrite proof of s ~ t in Roo,
which in turn implies that there is some proof Q in Ej U Rj, such that
P::}l Q.
In summary, any proof P which is not a rewrite proof in Roo can be
transformed to a simpler proof Q by::}l. By the induction hypothesis, the
proof Q, and hence P, can be transformed to a rewrite proof. Q.E.D.

A special case of compositeness is the following criterion suggested by

Kapur, Musser, and Narendran (1988).
Definition 2.38. Let R be a rewrite system. A critical overlap too +-;~::Ia
SU -+~1':::I1I su[vu]p is said to be prime if no proper sub term of sulp = uu is
reducible by R.
A critical pair is prime if its corresponding critical overlap is prime.
For example, if R contains rewrite rules (z- .y)- -+ y- ·z--, z·z- -+ e,
and z- - -+ z, then the first two rules define a critical overlap

which is not prime, because the subterm z-- in z- . z-- is reducible.

Kapur, Musser, and Narendran (1988) proved the soundness of a criterion
based on prime critical pairs, while Bachmair and Dershowitz (1988) es-
tablished its correctness. In fact, all (correct) criteria mentioned above are
special cases of the criterion PCP.
Various techniques can be used in practice to establish compositeness.
Let P be a critical overlap too +-;1':::16 SU -+~1':::I1I su[vu]p and suppose the
overlapped term su = su[uu]p is reducible, say su -+~:l':::Itl w.
 CRlTICAL PAIR CRlTERIA 37

If p' = pq for some position q, and either q i' A or else both s I> s' and
u I> s', then there is a binary decomposition PI P2 of P, where PI is the
>. pi pi P
peak tu ~t::=6 su -461::=t' w and P2 the peak w ~tl::=6' SU -4u::=v su[vu]p.
We have P >-C PI because

{( {su}, su, s, tu), ( {su}, uu, u, su[vu])}

>-~ul
{( {su }, su, s, tu), ({su }, uul q , s', w)}
and P >-c P2 because
{( {su}, su, s, tu), ({ su}, uu, u, su[vu])}
>-~ul
{( {su}, uul q , s', w), ({su}, uu, u, su[vu])}.

It should be noted that s I> s' indicates that the rule s - 4 t can be collapsed
(and hence no critical pairs need to be computed with it). In practice it is
therefore sufficient to require q i' A, which is the version of binary decompo-
sition that was introduced by Kapur, Musser, and Narendran (1988). Note
that such a decomposition exists whenever a critical pair is non-blocked.
If the position p' is not below q, additional information is required to en-
sure compositeness. Suppose that p' i' A and there is a proof P l of tu ~ w,
such that P >-c Pl. Define P2 to be the peak w ~R SU -4R su[vu], to ob-
tain a decomposition P l P2 of the original peak. The difficulty, of course, is
to determine whether a suitable proof P l exists. The techniques mentioned
above for checking for connectedness may for instance be employed for that
purpose.
A critical pair criterion may considerably decrease the total number
of critical pairs generated by completion. This advantage may be offset,
however, by the additional cost of checking whether the criterion applies to
a given critical pair. Experimental results that give some indication of the
utility of some critical pair criteria have been reported by Kapur, Musser
and Narendran (1988) and by Kiichlin (1985).
We conclude this section by establishing a Church- Rosser result via
compositeness. We say that a critical pair tu ~ su[vu]p of a rule u - 4 v on
s - 4 t at position p is subsumed by another critical pair tu' ~ su'[v'U']pl
of a rule u' - 4 v' on the same rule s - 4 t at a position p' if (i) p' i' A and
(ii) there exists a substitution T, such that xu = (XU')T, for all variables x
occurring in s. We say that 5 ~ CP(R) is a complete set of critical pairs
if each critical pair in CP(R) is subsumed by some critical pair in 5.
Proposition 2.39. Let R be a terminating rewrite system and 5 be a com-
p/ete subset of CP(R). If R is convergent on 5, then R is Church-Rosser.
38 STANDARD COMPLETION

Proof. It is sufficient to prove that all critical pairs in C P( R) \ 8 are com-

posite. Let tu R:l su[vu] be a critical pair in CP(R) \8, with corresponding
overlap P = tu +-t::u su -+~R$tI su[vu]p. Since 8 is complete, the corre-
sponding critical pair is subsumed by another critical pair tu' R:l su'[V'U']pl
of some rule u' -+ v' on s -+ t at position p', where p' "I A and there exists
= =
a substitution r, such that (tu')r tu and (su'[v' u']pl)r su[v' U]pl. Since
R is convergent on 8, there is a rewrite proof of tu' R:l su' [v' U']pl . Let
Pl be a corresponding rewrite proof of tu R:l su[v' U]pl and let P2 be the
proof su[V'U]pl +-~:R$tll su -+~R$tI su[vu]p. Evidently, P >-c Pl. Moreover,
P >-c P2 because
{( {su}, su, s, tu), ({ su}, uu, u, su[vu])}
>-~ul
{( {su}, u' u, u', tu), ({ su}, uu, u, su[vu])}

(note that u'u is a proper subterm of su). Therefore, P1 P2 is a decompo-

sition of P. Q.E.D.

This proposition has applications to rewrite systems containing rules

t[s, s]
-+ u with multiple occurrences of the same sub term on the left-hand
side. For each critical pair obtained by superposing on one occurrence of s,
there is a corresponding critical pair obtained by superposing on another
occurrence of s. As all these critical pairs subsume each other, it is sufficient
to compute only one of them. Such a critical pair criterion appears to be
particularly useful in associative-commutative completion, where rewrite
rules with multiple occurrences of identical subterms are common (Zhang
and Kapur, 1989).

Summary
We have reformulated the Knuth-Bendix completion procedure as an equa-
tional inference system and have introduced proof orderings as a technique
for reasoning about this and related equational inference systems. We have
also formulated refinements of completion based on critical pair criteria in
this framework. The key to this approach is the interpretation of completion
as a proof normalization process. We have designed proof transformations
to describe the effect of the inference rules on the proof level and defined a
suitable measure of the complexity of proofs to show that proof transforma-
tions are normalizing. The notion of fairness characterizes those sequences
of proof transformations for which normal-form proofs are rewrite proofs.
3. EXTENDED COMPLETION

Standard completion cannot be applied to equations, such as commutativ-

ity, for which the corresponding rewrite relation is non-terminating. There
are also limitations in applications to theories with associativity or similar
so-called permutative equations, as such theories often cannot be repre-
sented by finite convergent rewrite systems. For instance, from given rules

f(f(x,y),z) - f(x,f(y, z»
f(a, b) - b
f(a, f(x, b» - f(x,b)
completion may generate an infinite set of rules

f(a,f(x, f(y, b))) - f(x,f(y, b»

f(a, f(x, f(y, f(z, b)))) - f(x,f(y,f(z,b)))

as pointed out by Peterson and Stickel (1981). Associativity and commuta-

tivity are typical equations that are more naturally viewed as "structural"
axioms (defining a congruence relation on terms) rather than as "simpli-
fiers" (defining a terminating rewrite relation).
In such situations it is often more fruitful to construct, not necessarily a
convergent rewrite system, but instead a rewrite system for which normal
forms are unique only up to the congruence defined by given structural
axioms, such as associativity and commutativity. More precisely, given a
set of equations E, a set of structural axioms A is singled out, and then a
rewrite system R is constructed, such that A U R defines the same equa-
tional theory as E, and normal forms with respect to R are unique up to
the congruence generated by A. Huet (1980) proposed a corresponding
completion procedure which applies to left-linear rewrite systems.
A more drastic approach relaxes not only the convergence requirement,
but in addition extends the underlying rewrite relation to congruence classes
ofterms. Such extended completion procedures employ generalized versions
of matching and unification that are defined with respect to the given con-
gruence. Their advantage is that they also apply to non-left-linear systems.

39
40 EXTENDED COMPLETION

For example, if rewriting takes into account the associativity axiom

f(f(x,y),z) ~ f(x,f(y,z)), then the system consisting of the two rules
f(a, b) --+ band f(a, f(x, b)) --+ f(x, b) defines unique normal forms (up to
associativity).
Extended completion procedures have been developed for various con-
gruences. Basic concepts of the approach were described by Lankford and
Ballantyne (1977a, b, c) and Peterson and Stickel (1981), for rewriting
modulo associativity and commutativity. Jouannaud (1983) and Jouan-
naud and Kirchner (1986) demonstrated that a modified version of the
Peterson-Stickel procedure can be applied not only to associativity and
commutativity but to any equational theory with a finite, complete unifi-
cation algorithm, provided all congruence classes are finite.
In this chapter we formalize these approaches within the inference sys-
tem cum proof complexity framework. We describe the left-linear-rule
method and present an extended completion method that covers arbitrary
congruences, not just those for which congruence classes are finite. Before
we discuss these methods, we introduce some basic terminology.

3.1. Rewriting Modulo a Congruence

Let A be a given set of equations. (For simplicity, we assume that A is

symmetric, so that the two rewrite relations --+ A and <-+ A are identical.)
By [s] we denote the congruence class of s with respect to A; that is, [s]
is the set {t : s <-+A t}. For any rewrite system R, we denote by RIA (R
mod A) the set of all rewrite rules s --+ t, such that s <-+A U --+R v <-+A t,
for some terms u and v. The system RIA represents the rewrite relation
induced by R on congruence classes of A.
If congruence classes of A are finite (and an algorithm for enumerating
the elements of each congruence class is given), then reducibility of terms
by RIA is decidable, provided reducibility by R is decidable. To determine
whether a term t is reducible by RIA, simply check whether some term in
the congruence class of t is reducible by R. Since rewriting by RIA tends to
be inefficient (if decidable at all), a slightly weaker, but often more practical
notion of rewriting is usually employed within completion.
We say that a term t A-matches a term s if there is a substitution CT,
such that SCT <-+A t. The system RA consists of all rules s --+ t, such that
s <-+A UCT and t = VCT, for some rule U --+ v in R and some substitution
CT. The system RA is contained in RIA. It generalizes rewriting by R in
that it employs A-matching rather than ordinary matching. In this sense
we speak of rewriting modulo a congruence or extended rewriting. A term
t is reducible by RA if and only if some subterm of t A-matches a left-hand
 REWRITING MODULO A CONGRUENCE 41

side of a rule in R.
For example, if A consists ofthe associativity and commutativity axioms
for addition, and R contains rules -z + z --+ 0 and f(z, z) --+ z, then
f( z + y, y + z) is irreducible by R, but can be reduced to z + y by RA. The
term -z + (z + y) is irreducible by RA, but can be reduced to 0 + y by
RIA.
A reduction ordering >- is said to be compatible with A if u ~A s >-
t ~A v implies u >- v, for all terms s, t, u, and v. Any ordering >- that is
compatible with A induces an ordering (also denoted by >-) on congruence
classes of ~A: [s] >- [t] if s >- t. (This definition is valid precisely because
>- is compatible with A.) A rewrite system RIA is terminating if and only
if R is contained in some reduction ordering >- compatible with A.
A rewrite system R is said to be Church-Rosser modulo A if for all
terms sand t with s ~AUR t, there exist terms u and v, such that s --+R
u ~A v -R t. We say that R is convergent modulo A (or A-convergent) if
RIA is terminating and R is Church-Rosser modulo A. An A-convergent
system defines normal forms that are unique up to the congruence ~A'
If R is convergent modulo A and R' is any rewrite system with R ~
R' ~ RIA, then R' is also convergent modulo A and furthermore a term
is irreducible by R' if and only if it is irreducible by RIA. In particular, if
RA is convergent modulo A, then it defines the same normal forms as RIA.
Therefore RA can be used instead of RIA for the purpose of normal-form
computation.
The following example, given by Huet (1980), illustrates these notions.
Let A be the set consisting of the associativity and commutativity axioms
z+y ~ y+z z·y ~ y·z
z + (y+ z) ~ (x + y) + z z . (y . z) ~ (z.y).z
and let R be the rewrite system
z+O --+ z z ·1 --+ x
O+x --+ z 1· x --+ x
f(O) --+ 1 f(z + y) --+ f(z)· f(y)
The system RIA is terminating. (Termination can be proved by an as-
sociative path ordering, Bachmair and Plaisted 1985.) Furthermore, R
is Church-Rosser modulo A (a test for the Church-Rosser property is de-
scribed below).
In the remaining sections of this chapter, we shall study methods for
constructing a rewrite system R for a given set of equations E, such that
A U E and A U R define the same equational theory and a certain rewrite
system R', with R ~ R' ~ RIA, is convergent modulo A. (Two cases will
=
be considered: R' Rand R' RA') =
42 EXTENDED COMPLETION

3.2. The Left-Linear Rule Method

Following the approach outlined in the previous chapter, we discuss Huet's
method for constructing A-convergent rewrite systems from the perspective
of proof normalization. We assume that all equations in A are of the form
s ~o t, while other equations are labelled by the symbol T or ..L. As before,
equations S~.l t are called rewrite rules and written s - t.
In this context, a normal-form proof is a rewrite proof modulo A in R;
that is, a proof of the form s -'R v +-+~ w ~'R t. As before, by a peak
we mean a proof s ~ R U - R t. By a cliff we mean a proof of the form
s +-+A U - R tor s ~R U +-+A t.
A rewrite system R is Church-Rosser modulo A if and only if there is
a rewrite proof modulo A in R for every equation provable in A U R. A
proof in Au R, on the other hand, is a rewrite proof modulo A if and only
if it contains neither a peak nor a cliff. The Critical Pair Lemma indicates
that a peak s ~ R U - R t can either be replaced either by a rewrite proof
s -R v ~R t or by a critical-pair proof s +-+CP(R) t.
Let P be a cliff s +-+A U - R t. If P is a proper overlap, then by the
Critical Pair Lemma we have s ...... CP(AUR)\CP(A) t. If P is a non-overlap,
then a rewrite proof modulo A can be obtained by commuting the two
proof steps. That is, there is a term v, such that S - R v +-+A t. Also,
any variable overlap s +-+ A U - R t in which the second proof step applies
below the first, can be replaced by a rewrite proof modulo A of the form
s -'R v +-+A W ~R t (cf. the Critical Pair Lemma). Unfortunately, similar
variable overlaps in which the first proof step applies below the second can
be problematic, as there may exist only a proof S ...... :A v - R W +-+:A t, but
not necessarily a rewrite proof modulo A.
For example, the equation a ~ b and the rule x . x - x determine a
variable overlap

that can only be replaced by a proof

but not by a rewrite proof modulo A. The first two proof steps

in this proof form a variable overlap that can be replaced by a proof

which contains the initial variable overlap as a subproof.

 THE LEFT-LINEAR RULE METHOD 43

,
. ....

Figure 3.1: Left-linear variable overlap

This example involves a non-left-linear rewrite rule. In fact, a variable

overlap s +-+ A U - R t, wherein the first proof step is below the second, can
always be replaced by a rewrite proof modulo A, if the proof step U - R t is
by application of a left-linear rewrite rule (see Figure 3.1 and compare with
Figure 2.3). In short, the proof simplification techniques we have outlined
in the previous chapter can be directly applied to extended completion,
provided all (persisting) rewrite rules are left-linear.
Let >- be a reduction ordering that is compatible with A. The inference
system C~ differs from the standard completion system C>- only in the
following inference rules:
EjR
DEDUCTION: if s ~ t E CP(A U R)
EU{s~t}jR

EU{s~s}jR
DELETION: if s +-+:A t
EjR
where R may be any rewrite system ordered by >-. The inference rules
for orientation, simplification, composition, and collapse are the same as
for standard completion. Thus, if A = 0, then C~ is essentially the same
as the standard completion system C>-. (The only difference is that the
present deduction rule, being formulated in terms of critical pairs, is more
restrictive than the corresponding inference rule of standard completion.)
Inference systems CA are called left-linear completion systems. They
are sound in the following sense.
44 EXTENDED COMPLETION

Lemma 3.1. Whenever E ; R I- C.A E'; R', then the two congruence rela-
tions +-+ AuEuR and +-+AuE'uR' are the same.
The above deduction rule is reflected by proof transformation rules

S+-RU-+R t => s+-+E t

S +-+ A U -+R t => S +-+E t
while the new deletion rule is reflected by proof transformation rules

The remaining transformation rules, for orientation, simplification, compo-

sition, and collapse, are the same as for standard completion.
By 'R.~ (or simply 'R.c., if>- is clear from the context) we denote the
set of all these transformation rules. The corresponding transformation
relation is denoted by => c..
Lemma 3.2. The proof transformation system 'Ilc. reflects the inference
system c.

Lemma 3.3. The transformation relation =>c. induced by'R.c. is terminat-

mg.

Proof. We define a proof ordering >-c. to prove termination of => c.. The
ordering is based on suitable a measure of the complexity of a proof. The
cost of a proof step s +-+~~"II t is defined to be:

({[sl,[tn,T,1.) ifn=T
{ ({[sl, [tn, 1.,1.) if n = 0
({[sn, u, ([tn) if n = 1. and U>- v
({[tn, v, ([sn) if n = 1. and v >- u
The complexity of a proof is the multiset of all costs of its proof steps.
Again, a proof P has the same complexity as the inverse proof p- 1 •
Let >-' be the lexicographic combination of the multiset extension of the
reduction ordering >-, the encompassment ordering 1>, and the reduction
ordering >-. We assume that the symbols 1. and T are minimum and
maximum elements in any ordering. Proofs are compared with respect
to their complexity, using the multiset extension of the ordering >-'. The
resulting ordering, which is a proof ordering, is denoted by >-c.. It contains
the transformation system'R.c. (and hence =>c.). The proof is similar to the
proof of Lemma 2.20 in the case of those transformation rules that have
been directly taken from standard completion--orientation, simplification,
composition, and collapse. We discuss the remaining cases in detail.
 THE LEFT-LINEAR RULE METHOD 45

i) Deduction. We have s +-R U -+R t >-.c S +-+E t, because u >- sand

u >- t. Furthermore, if u >- t then
({[S], [u]},.1,.1) >-' ({[s], [tn, T, .1),

which implies S +-+A U -+R t >-.c S +-+E t.

ii) Deletion. We have S +-+E t >-.c S +-+:A t, because ({[s], [tn, T,.1) >-'
({[u], [vn,.1,.1, whenever s +-+:A u and v +-+:A t. Q.E.D.

In analogy to Lemma 2.11 (and using similar arguments in the proof)

we obtain:

Lemma 3.4. If P is a peak s +-R u -+R t, a cliff s +-+A U -+R t, or a cliff

s +-R U +-+A t, and Q is a rewrite proof modulo A of s ~ t, then P Q. =>c
The transformation relation =>.c also provides a way to prove the fol-
lowing Church-Rosser theorem.

Theorem 3.5. (Huet 1980) Let R be a rewrite system and A be a set of

equations, such that R/A terminates. The system R is Church-Rosser mod-
ulo A if and only if, for all terms sand t with s +-R U -+AuR t, there exist
terms v and w, such that s -+:R v +-+:A w +-:R t.

Proof. If R is Church-Rosser modulo A, then evidently any peak or cliff

can be replaced by a rewrite proof modulo A.
On the other hand, suppose that every peak or cliff can be replaced by a
rewrite proof modulo A. Let >- be the reduction ordering -+~/A induced by
RIA and =>! be the transformation relation associated with n~. We prove
by induction on =>! that every proof in A U R can be transformed into a
rewrite proof modulo A in R. If a proof P in A uRis not a rewrite proof
modulo A, then it must contain a peak s +-R U -+R t, a cliff s +-+A U -+R t,
or a cliff S +-R U +-+ At. By our assumption, for any such peak or cliff there
exists a rewrite proof modulo A of the form s -+:R v +-+:A w +-:R t. Using
Lemma 3.4, we may infer that there is a proof Q, such that P =>!
Q. By
the induction hypothesis, the proof Q (and hence P) can be transformed
into a rewrite proof modulo A. Q.E.D.

Let us emphasize that this theorem applies to arbitrary rewrite systems

R, not just left-linear systems. Left-linearity will be crucial, however, in
deriving effective conditions under which all cliffs can be transformed to
rewrite proofs modulo A.
By N,£ we denote the set of all rewrite proofs modulo A. We can now
formulate a sufficient condition for fairness.
46 EXTENDED COMPLETION

Lemma 3.6. A non-failing derivation Eo; Ro I- c E 1 ; Rl I- c ... is fair

with respect to 'Rc and Nt:. if Roo is left-linear and the set of critical pairs
CP(AURoo)\CP(A) is a subset of the set of all deduced equations Uk Ek.

Proof. Let Eo; Ro I- t:. El ; Rl I- t:. .•. be a derivation for which Eoo = 0,
Roo is left-linear, and CP(A U Roo) \ CP(A) is a subset of Uk Ek. We
have to show that whenever a proof P in A U Eoo U Roo contains a peak
Sf-Roo U -Roo t, a cliff s ...... A U -Roo t, or a cliff Sf-Roo U ......A t, then
there is a proof Q in Ui A U Ei U Ri, such that P =?! Q.
By the Critical Pair Lemma, any peak or cliff in P which is a non-
overlap or variable overlap can be replaced by a rewrite proof modulo A.
(As we have pointed out above, it is essential in the variable-overlap case
that all rules in Roo be left-linear.) Since CP(AURoo)\CP(A) is a subset
of Uk Ek, every proper overlap can be replaced by a simpler proof, from
which the assertion can be inferred easily. Q.E.D.

Lemmas 3.2, 3.3, and 3.6 indicate that Theorem 2.10 can be applied to
the inference system £, the proof transformation system 'Rt:., and the set
of proofs Nt:..

Theorem 3.7. Let Ro be a rewrite system and )- be a reduction ordering

that contains Ro and is compatible with A. If Eo ; Ro I- c El ; Rl I- t:. ..• is a
derivation for which Eoo = 0, Roo is left-linear, and CP(A U Roo) \ CP(A)
is a subset of Uk Ek, then Roo is convergent modulo A.

The main limitation of the above completion method is that only left-
linear convergent rewrite systems can be produced. Rewrite systems with
rules such as x- . x - 0 or x . x - x are not within its scope. Indeed, to
eliminate variable overlaps that result from non-left-linear rules, so-called
"variable instance pairs" would have to be computed (see Bachmair, Der-
showitz, and Hsiang 1986).
For instance, the variable overlap a . b ...... A a . a - R a, determined by
the equation a ~ b and the rule x . x - x, defines a variable instance pair
a . b ~ a. More precisely, the equation a . b ~ a is obtained by superposing
the equation a ~ b on the instance a . a - a of the rule x . x - x.
Exhaustive computation of variable instance pairs is impractical in gen-
eral. An alternative, which we shall pursue in the remaining sections of
this chapter, is to approximate rewriting on congruence classes by the ex-
tended rewrite relation R A . Then each problematic variable overlap can
be regarded as a single rewrite step. For instance, the variable overlap
a . b ...... A a· a - R a corresponds to an extended rewrite step a . b - R A a.
Rewriting modulo a congruence thus avoids problematic variable overlaps,
but presents the difficulty of eliminating more general overlaps involving the
 CHURCH-ROSSER SYSTEMS 47

extended rewrite relation RA . For many sets of equations A, such extended

overlaps can be effectively eliminated.

3.3. Church-Rosser Systems

We first consider under which conditions an extended rewrite system RA is
convergent modulo A. By Ne we denote the set of all rewrite proofs modulo
A in RA, that is, proofs of the form 8 -RA U +-+::4 V -RA t, where R is a
rewrite system contained in the given reduction ordering >-. (The reduction
ordering is assumed to be compatible with A, so that R/A is terminating.)
A rewrite system RA is Church-Rosser modulo A if and only if there
is a rewrite proof modulo A in RA for every equation valid in AURA. A
proof in AURA, on the other hand, is a rewrite proof modulo A in RA if
and only if it contains no peak 8 -RA U -RA t and no cliff 8 +-+A U -RA t
(or the inverse of such a cliff). If RA is Church-Rosser modulo A, then
every peak or cliff can be replaced by a rewrite proof modulo A. If R/A
is terminating, the converse direction is also true. That is, if RA is not
Church-Rosser modulo A, then some peak or cliff can not be replaced by a
rewrite proof modulo A.
The Critical Pair Lemma, when applied to the rewrite system RA, in-
dicates that non-overlaps and variable overlaps can always be replaced by
rewrite proofs, while proper overlaps 8 -RA U - RA t can be replaced by
proofs 8 +-+CP(RA) t. Since the set CP(RA) is in general infinite, this does
not yield a practical method for dealing with proper overlaps. (Of course,
the same difficulty also arises with cliffs 8 +-+A U -RA t.) We shall therefore
deal with systems RA indirectly, via R, by regarding 8 -RA t not as an
elementary proof step in RA, but instead as a proof 8 +-+::4 8' -R t in AUR.
More precisely, by 8 +-+~P t we denote a proof
8 = Uo ~l
el Ul ~2
e2 U2 ~3
e3 ••• U n -1 ~eft.. fl_
.... =t
where all positions PI, ... ,Pn are below P and all equations el, ... ,en are in
E. Similarly, we write 8 +-+~p t, if the positions PI, ... ,Pn are strictly below
p. By 8 -RA t we mean a proof 8 +-+~P U ~ t, where e is an equation in
R. Thus, when speaking of a peak 8 -RA U -RA t, we are referring to a
proof 8 ~ 8' +-+~P U +-+~q t' _:, t, where e and e' are equations in R.
Consider such a peak
8 -1?e 8' +-+~p U +-+~q
A A
t' -qe" t
where the position P is not strictly below q. This proof can be written
either as
48 EXTENDED COMPLETION

or as
s ~,
e S
<p
+-+A U
p',
+-+ell <q t'
U +-+A
q t
-e"

where e" is an equation in A and the position p' is not below q.

Henceforth, by a peak S - R U - RA t we intend a proof

S ~e U +-+A<q t' - qe' t ,

where p is not strictly below qj by a cliff S +-+ A U -RA t, a proof

where p is not below q.

The above considerations indicate that a proof is a rewrite proof modulo
A in RA if and only if it contains no peak or cliff (or the inverse thereof). We
shall next describe which peaks and cliffs can always be replaced by rewrite
proofs modulo A and describe techniques to eliminate "problematic" peaks
and cliffs.
A peak s -{;,~v U +-+~q t' -:,~W, t, where p is not strictly below q, is
called a non-overlap if p and q are disjoint positions. On the other hand, if
q = pp', for some position p', then P is called a (extended) proper overlap
if p' is a non-variable position in Vj and a (extended) variable overlap,
otherwise. The same classification is applied to cliffs s ~ U +-+~q t' -:, t
where p is not below q. If such a cliff is a variable overlap or proper overlap,
then q is a position strictly below p. Non-overlaps and variable overlaps
can be replaced by rewrite proofs modulo A in the following way.
A non-overlap s -~~V U +-+~q t' -:,~W, t is a proof of the form
u[Q]pu[Q']q, where Q is the proof sip -!~V ulp and Q' the proof ulq +-+A
t'lq -:,~W, tlq· The alternative proof s[Q']qt[Q]p is a rewrite proof modulo
A. We associate the transformation rule

with the non-overlap.

If s -w~v
p <q t' -v'~w'
U +-+A q t 'IS a vana . ble over Iap, then q pq ' q" , =
where vlq' = x, for some variable x. Let 0' be a substitution, such that
ulp = VO' and sip = WO'o Let Q be the subproof s -{;,~v U and Q' be the
proof
=
xu U Ipq' +-+A<qll'l q"
t pq' -v,~w, t Ipq' U ' =
so that the variable overlap is the composition of Q with the proof u[Q']pq"
Let now Pl,"" Pn be all the positions in w at which the variable x
= =
occurSj and let So sand Si s[u', ... , U']pPl •...•pp;, for all i with 1 $ i $ n.
By Pi we denote the proof Si-l[Q']pp;. Note that Pi is a proof of Si-l ~ Si.
 CHURCH-ROSSER SYSTEMS 49

Similarly, let Ql,' .. , qm be all the positions in v, other than q', at which x
= =
occurs; and let to t and ti t[u', ... , u']Pfl> ... ,Pfi' for all i with 1 ~ i ~ m.
By Qi we denote the proof ti-dQ']Pfi' Note that Qi a proof of ti-1 ~ ti.
=
Furthermore, let p be a substitution for which xp u' and yp yu, if =
= =
y:/= x. Then tml p vp and Sn tm[wp]p. Consequently, there is a proof
Q" = Sn +-+~~tI t m •
We associate with the variable overlap the proof transformation

which transforms the variable overlap into a rewrite proof modulo A. (Note
that n is the number of occurrences of x in wand m + 1 is the number of
occurrences of x in v.)
The above proof transformations apply to non-overlaps and variable
overlaps-peaks and cliffs. If complete sets of A-unifiers can be computed,
then proper overlaps can also be dealt with effectively.
Two terms sand t are said to be A-unifiable if there exists a substitution
u, called an A-unifier, such that su +-+A tu. A set E of A-unifiers of
S and t is said to be complete if for every A-unifier T of sand t there
exist substitutions u in E and p, such that XT +-+A (xu)p, for all variables
x occurring in s or t. (We may assume without loss of generality that
whenever u is an element of a complete set of A-unifiers of sand t, then
xu = x, for all variables x not occurring in s or t.) A set E of A-unifiers of
sand t is said to be minimal if, given any two distinct substitutions u and
Tin E, there is no substitution p, such that XT +-+A (xu)p, for all variables
x in s or t.
Finite, complete sets of unifiers need not exist for arbitrary sets of equa-
tions (Plotkin 1972). There are also theories for which minimal, complete
sets of unifiers do not always exist (Fages and Huet 1986). However, if there
is a finite, complete set of unifiers, then there is a minimal one. Minimal,
complete sets of unifiers are also unique in a certain sense (for details see
Fages and Huet 1986). Algorithms for computing minimal, complete sets of
unifiers are known for many theories of practical importance, including com-
mutativity (Plotkin 1972); associativity and commutativity (Stickel 1981;
Fages 1987); and associativity, commutativity, and identity (Fages 1987).
If A is the empty set, then the set consisting of a most general unifier of s
and t is complete. For a survey on unification, see Siekmann (1984). More
recent results and further references can be found in Kirchner (1986, 1988)
and Gallier and Snyder (1990).
Henceforth, we shall assume that A is a set of equations for which
minimal complete sets of unifiers exist.

Definition 3.8. Let u ~ v and s ~ t be equations with no variables in

50 EXTENDED COMPLETION

common (if necessary, the variables of one equation are renamed) and let
p be a non-variable position in u, such that ulp and s are A-unifiable with
minimal complete set of unifiers E.1 By an A-critical overlap we mean any
proof vu +-!r:=u uu -~P uu[su]p -~r:=t uu[tu]p, where u E E. The equation
vu ~ uu[tu]p is called an A-critical pair.

In other words, A-critical pairs differ from ordinary critical pairs in that
A-unification is used instead of unification. By CPA(E) we denote the set
of all A-critical pairs between equations in E. By CPA(E, A) we denote
the set of all A-critical pairs of equations in E on equations in A.
By the (left) variable part of a proof step s -~'r:=t' t we mean the set of
all positions pqr in s, for which s'lq is a variable. (The right variable part
is the set of all positions pqr in t, for which t'lq is a variable.)

Lemma 3.9. (Extended Critical Pair Lemma, Jouannaud 1983) Let R be

a set of equations and suppose complete sets of A-unifiers can be computed.
(1) If s +-AuR U -RA t is a non-overlap or variable overlap, then there
exists a rewrite proof s -RA v +-+:A W +-RA t.
(2) If s +-AuR u - RA t is a proper overlap, then there exists a proof
s +-+:A s' +-+CPA(R)UCPA(R,A) t' +-+:A t in which all proof steps in s +-+:A v
apply in the variable part of s +-AuR u.

Proof. We have already proved the first part of the lemma. For the second
part, let P be a proper overlap s +-{;,r:=v U +-+~q t' -!'r:=w' t, where q pq', =
for some position q'. (We may assume, without loss of generality, that
v ~ wand v' ~ w' have no variables in common.) Let u be a substitution,
such that ulp = =
vu and ul q v'u. Since vlq' is A-unifiable with v', there
is a complete set of A-unifiers E. Let TEE and p be substitutions, such
that WT ~ VT[W'T]q' is an A-critical pair and xu +-+:A XTP, for all variables
x in v ~ W and v' ~ w'. As a consequence, we have sip -:A WTP and
tip +-+:A VTp[W'Tp]q" which implies that there is a suitable proof s +-+:A
s' -CPA(R)UCPA(R,A) t' -:A t. Q.E.D.

The Extended Critical Pair Lemma serves as the basis for a Church-Rosser
result for extended rewrite relations RA.

Definition 3.10. The subterm ordering modulo A is defined by: s tA t

if some subterm of s is equivalent to t in A. The encompassment ordering
modulo A is defined by: s t> A t if either s t> t or else s +-+~), s[tu], for some
substitution u.
1 We may assume that for each fT in E and variable x in u or &, the tenn XfT contains
none of the variables occurring in & or u r:= tI.
s::::I t
 CHURCH-ROSSER SYSTEMS 51

In other words, s I> A t if either s is a proper instance of t or else some

proper subterm of s is equivalent with respect to A to an instance oft. The
relation I> A is not well-founded in general, but we have:

Lemma 3.11. The encompassment ordering modulo A is well-founded if

and only if the (strict part of the) subterm ordering modulo A is weI/-
founded.

Proof. Clearly, if the encompassment ordering modulo A is well-founded,

so is the subterm ordering modulo A. On the other hand, suppose the
encompassment ordering modulo A is not well-founded. Since the stan-
dard encompassment ordering is well-founded, there exists an infinite se-
quence of ground terms t l , t 2, t3, ... and a corresponding sequence of posi-
tions Pl,P2,]J3, ... such that, for all i, Pi f: A and ti+l +-?A tilp;. Thus the
subterm ordering modulo A is not well-founded. Q.E.D.

Note that if the subterm ordering modulo A is well-founded, then all con-
gruence classes of A have to be finite.

Theorem 3.12. (Jouannaud and Kirchner 1986) Let A be a set of equa-

tions for which minimal complete sets of A-unifiers can be computed, and
let R be a rewrite system such that RIA is terminating. If the subterm
ordering modulo A is well-founded, then RA is Church-Rosser modulo A
if and only if for all A-critical pairs s ~ t in CPA(R) U CPA(R,A), there
exist terms s' and t', such that s - RA S' +-? At' .-RA t.

Proof. The only-if direction is trivial. To prove the if-direction we first

define a well-founded ordering )- A,R on proofs in AU R.
Let)- be the reduction ordering -~/A induced by RIA and let P be a
proof
to~: tl ~~ t2 ~: .. ·tn-l ~: tn
in A U R, where ei is an equation Ui ~ Vi.
The i-th proof step in P is said to be bound on the left if P contains
a subproof tj-l '-R A ti, and bound on the right if it contains a subproof
ti-l -RA tj. We define: fJ{ = 0, if the i-th proof step in P is bound on
the left and right; fJ{ = 1, if it is either bound on the left or on the right,
but not both; and fJ{ = 2, otherwise.
The complexity of single proof steps in P is defined by:

if Ui ~ Vi E A
if Ui ~ Vi E R
if Vi ~ Ui ER
52 EXTENDED COMPLETION

The complexity of a proof is the collection of all tuples associated with

its proof steps. 'fuples are compared lexicographically, using the multiset
extension >-mul of the reduction ordering >- in the first component, the
encompassment ordering modulo A in the second component, and the usual
greater-than relation in the last component. Proofs are compared according
to their complexity, using the multiset extension of this ordering on tuples.
We denote the corresponding ordering on proofs by >- A,R. If the proper
subterm ordering modulo A is well-founded, then >- A,R is well-founded.
In general, >- A,R is not a proof ordering, as the third component of the
complexity of a proof step depends on the context in which a proof step
appears.
We show that all minimal (with respect to >- A,R) proofs in Au R are
rewrite proofs modulo A. If P is a minimal proof, but not a rewrite proof
modulo A, it contains either a peak s +-R U --+RA t or a cliff s +-+A U --+RA t
(or the inverse of such a cliff).
Peaks. By the Extended Critical Pair Lemma, any peak P' = s +- R
U --+ RA t can be replaced by a proof P" in which all terms are strictly smaller
than u, so that P' >- A,R P" and, as can easily be seen, also P[P'] >- A,R
P[P"].
Cliffs, non-overlaps. A non-overlap is a proof P' = u[Q]pu[Q']q, where
Q is a proof sip +-~I'i:SV ulp in A and Q' is a proof ulq +-+A t'lq --+;/I'i:SWI tlq in
AU R. Any such non-overlap can be replaced by a proof P" = s[Q']qt[Q]p.
Since u[Q']q has the same complexity as s[Q']q and u[Q]p >- A,R t[Q]p, we
have P' >- A,R P". It can easily be checked that also P[P'] >- A,R P[P"].
Cliffs, variable overlaps. A variable overlap is a proof of the form P' =
Qu[Q']pql which, as we have shown above, can be replaced by a proof P" of
the form Pl· ··PnQ"Qm·· ·Ql. Since RIA is terminating, we have n > O.
Since Q >-A,R P" we have P' >-A,R P" and also P[P'] >-A,R P[P"].
Cliffs, proper overlaps. By the Extended Critical Pair Lemma, every
proper overlap P' of the form

s ~WI'i:SV u +-+A
<q t' q
--+V 'I'i:SW I
t,
where v R:I w is an equation in A and v' R:I W' is a rule in R, can be replaced
by a "critical-pair proof" s +-+A s' +-+CPA(R,A) t' +-+A t, where all proof steps
in s +-+A s' apply in the variable part of s +-~I'i:SV u. Moreover, the stated
assumptions guarantee that there is a rewrite proof modulo A of s' R:I t'.
Observe that w cannot be a variable, for otherwise the subterm ordering
modulo A would not be well-founded. As a consequence, the variable part
of s +-~I'i:SV u contains only positions strictly below p. Hence, there is a
proof P" of the form
 CHURCH-ROSSER SYSTEMS 53

We have
f) <p I
S --Wl::!11 U ~A,R S +-+A S

(using the second proof complexity component);

S .....yWl::!11 U ~ A,R SI ......R

• A S"

(using all three proof complexity components); and

S --Wl::!11
f) U ~A,R S " +-+A
• t" • t'
+-RA • t
+-+A

(using the first proof{;omplexity component). In sum, we have pI ~ A,R P"

and, as can easily be checked, also P[P ' ] ~ A,R P[P"]. Q.E.D.

Computation of A-critical pairs is the basis of extended completion pro-

cedures. While A-critical pairs are invariably used to eliminate peaks, dif-
ferent mechanisms have been suggested for elimination of cliffs. Consider a
proper overlap

where v ~ w is an equation in A and v' ~ w' is a rewrite rule in R. Then

q = pq/, for some position q' i= A, such that v Iql is not a variable and is
A-unifiable with v'. Placing the rule v' ~ w' in a larger context, we obtain
a new rule V[V']ql ~ V[W']ql and a corresponding proof

so that S ...... R' t, where R' = RU {V[V']ql ~ V[W']q/}. In other words, the
A
cliff has been eliminated.

Definition 3.13. (Jouannaud and Kirchner 1986) Let S ~ t be a rewrite

rule and U ~ v be an equation in A that has no variables in common with
S ~ t, such that some proper non-variable subterm ul p is A-unifiable with
s. Then u[s]p ~ u[t]p is called an extended rule of S ~ t with respect to A.

By EXTA(R) we denote the set of all extended rules of R with respect to A.

Extended rules were originally introduced by Peterson and Stickel (1981)
in the context of associative-commutative rewriting. We emphasize that
computation of extended rules does not involve A-unification. It suffices
to know that ulp and S are A-unifiable, but the actual A-unifiers need not
be computed. Extended rules are therefore often easier to compute than
A-critical pairs.
For example, a rewrite rule can be extended with respect to the asso-
ciativity axiom x + (y + z) ~ (x + y) + z if and only if its left-hand side
54 EXTENDED COMPLETION

is unifiable under associativity with y + z or z + y, which is the case if

the rule is of the form 8 + t -+ u. The corresponding extended rules are
z+ (8+t) -+ z+u and (8+t)+Z -+ u+z. Note that there are no extended
rules with respect to commutativity axioms z+y ~ y+z, as such equations
contain no proper non-variable subterms.

3.4. Extended Completion

We will next formulate extended completion as an equational inference
system. Some of the inference rules are designed so that equations can be
kept fully simplified and redundant equations can be deleted. For instance,
in the presence of 8 -+ t a rewrite rule U[8] -+ u[t] is usually redundant and
can be removed. However, extended rules serve a special purpose and have
to be exempted from this deletion mechanism. Therefore we partition a
given rewrite system R into two sets Nand S, where rules in S are protected
from certain simplification mechanisms. Formally, an unprotected rule is
an equation 8 ~.l. t, while a protected rule is an equation 8 ~l t. Equations
in A are of the form 8 ~o t; all remaining equations are of the form 8 ~T t.
An inference rule, in this co~text, is a binary relation on tuples E; N; S,
where N contains all unprotected rules and S all protected rules.
Let >- be a reduction ordering that is compatible with A. The inference
system C~ (or simply C) contains the following inference rules:
E;N;S
DEDUCTION: if8~tECPA(AUR)
EU{8~t};N;S

E;N;S
EXTENSION:
E;N;SU{8-+t}

EU{8~t};N;S
ORIENTATION: if 8>- t
E;NU{8-+t};S

E;NU{8-+t};S
PROTECTION:
E;N;SU{8-+t}

EU {8 ~ t};N;S
DELETION:
E;N;S
=
where R NUS denotes a rewrite system contained in >-. The following
inference rules, which are also part of C~ , are indispensable for efficiency:

EU{8~t};N;S
SIMPLIFICATION:
EU{u~t};N;S
 THE EXTENDED RULE METHOD 55

EjNU{s-+t}jS
COMPOSITION: if t -+R/A u
EjNU{s-+u}jS

EjNjSU{s-+t}
if t -+R/A u
EjNjSU{s-+u}

EjNU{s-+t}jS 'f <p, p

COLLAPSE: 1 S +-+ji S -+v::=w U,
EU{u~t}jNjS
for some rule v -+ w in
R, where s ~ v
where ~ may be any well-founded ordering on terms, e.g., the encompass-
ment ordering t>. The difference between protected and unprotected rules
is that collapse inferences may be applied only to the latter.
Inference systems t:A are called extended completion systems. Standard
completion can be simulated by extended completion: let A be the empty
set and ~ be the encompassment ordering, and consider only tuples Ej N j 0.
Inference systems t: are sound:
Lemma 3.14. If Ej Nj S rCA E'j N'j S', then the two congruence relations
+-+AUEUNUS and +-+AUE/UN/US' are the same.

If EjNjS rc E'jN'jS' and the reduction ordering >- contains NUS,

then >- also contains N' US' (recall that the ordering >- is compatible with
A). Consequently, the limit rewrite system (Nco U Sco)/A is terminating
for any derivation for which the initial rewrite system No U So is contained
in the reduction ordering >-. Furthermore, if EjNjS rc E'jN'jS', then
any term that is reducible by (N U S)/A is also reducible by (N' U S')/A.
Definition 3.15. By an A-completion procedure we mean a program that
accepts as input a reduction ordering >-, a set of equations Eo, and a rewrite
system Ro = No U So contained in >-j and uses the inference rules of t:~ to
generate a derivation from Eoj Noj So.
Definition 3.16. We say that an A-completion procedure fails for a given
input, if Eco =1= 0. It is correct, if (Nco U Sco)A is convergent modulo A,
whenever Eco = 0.
We shall use proof orderings to derive sufficient conditions for the correct-
ness of A-completion procedures.

3.5. The Extended Rule Method

Peterson and Stickel (1981) designed an A-completion procedure, for sets A
of associativity and commutativity axioms, that is characterized by the sys-
tematic use of extended rules. We demonstrate that similar techniques can
56 EXTENDED COMPLETION

be applied to arbitrary sets of equations A for which minimal complete sets

of unifiers exist. That is, we will show that suitable requirements regarding
the computation of extended rules ensure the fairness and correctness of
A-completion procedures.
First we design a suitable proof transformation system reflecting ex-
tended completion. Let A be the given set of equations, >-- be a reduction
ordering compatible with A, and > be a well-founded ordering.
Extension is reflected by transformation rules

u[s]p -~I'IS.1.t u[t]p ~ u[s]p -~['ll'lSlt1[tl u[t]p

u[s]p -~l'ISlt u[t]p ~ u[s]p -~['ll'lSlt1[tl u[t]p
where s >-- t and p =I A.
Orientation and protection are reflected by transformation rules
s -:I'ISTt t ~ s -:I'IS.1.t t
s -:I'IS.1.t t ~ s -:l'ISlt t
where s >-- t.
Deletion is reflected by
S+-+Et ~ s+-+At.
Simplification is reflected by

S +-+E t ~ S -RIA U +-+E t

(where S -RIA U denotes a proof S +-+A S' -R u' +-+A u).

Composition is reflected by
S -~.1.t t ~ S -~.1.tI U +-RIA t
S -:l'ISlt t ~ S -:l'ISlt1 u +-RIA t

where S >-- t and s >-- u.

Collapse is reflected by

where s >-- t, v >-- w, s > v, and either n = .1 or n = l.

The computation of A-critical pairs of CPA(R), which is part of deduc-
tion, is reflected by transformation rules

The other part of deduction-the computation of A-critical pairs of

CPA(R, A)-is not required with the extended rule method, as all cliffs
that are proper overlaps are eliminated by extended rules.
 THE EXTENDED RULE METHOD 57

By 'Ri we denote the set of all these proof transformation rules, plus
the transformation rules for elimination of cliffs that are non-overlaps or
variable overlaps. (The transformation rules for elimination of cliffs have
to be included, even though they do not reflect any inference rules.) By
~e we denote the corresponding transformation relation.

Lemma 3.17. If P is a peak s "-R U - R A t and Q is a rewrite proof

modulo A of the form s -RIA v f-+A W "-RIA t, then P ~t Q.

The analogous property for cliffs S f-+

A U - RA t does not hold, as the
transformation relation ~e is too weak. It is an open question whether 'Re
can be extended to a terminating transformation system in which a cliff
can always be transformed to a corresponding rewrite proof modulo A.

Lemma 3.1S. The transformation system 'Re reflects the extended com-
pletion system £..

Lemma 3.19. The transformation system 'Re is terminating.

Proof. We design a well-founded ordering >-e that contains ~e. Let P be

a proof
to f-+~: tl ~~ t2 f-+~: .. ·tn-l ~: tn
where ei is an equation Ui ~ni Vi.
The i-th proof step in P is said to be bound on the left if, for some j < i,
we have nj = 1, while njH = ... ni = 0 and all positions Pj+b··· ,Pi are
below Pj. (In other words, P contains a subprooftj_l "-SA ti.) The proof
step is bound on the right if, for some j > i, we have ni = ... nj-l = 0,
nj = 1, and all positions Pi, ... , Pj -1 are below Pj. (That is, P contains a
subproof ti-l -SA ti.) We define: f3{ = 0, if the i-th proof step in P is
bound on the left and right; f3{ = 1, if it is either bound on the left or on
the right, but not both; and f3{ = 2, otherwise.
The complexity of single proof steps in P is defined by:

({[ti-d, [ti]},.1,.1,.1,.1) ifni=T

({[ti-l]), ui,.1,.1, [tiD if ni = .1 and Ui >- Vi
({[ti])' Vi,.1,.1, [ti-l]) if ni = .1 and Vi >- Ui
({[ti-Il},.1, f3{,.1, [ti]) ifni=O
({[ti-l]},.1,.1, Ipil, [tiD if ni = 1 and Ui >- Vi
({[ti]}'.1,.1, Ipil, [ti-d) if ni = 1 and Vi >- Ui

where Ipi denotes the length of the sequence P (i.e., the depth of the redex
in the term) and f3{ is as defined previously. The complexity of a proof is
the collection of all tuples associated with its proof steps.
58 EXTENDED COMPLETION

Complexity tuples are compared lexicographically by the multiset exten-

sion >-mul of the reduction ordering >- (in the first component), the ordering
t> (in the second component), the greater-than relation on the natural num-
bers (in the third and fourth component), and the reduction ordering >- (in
the last component). We denote this lexicographic ordering by >-e. Proofs
are compared according to their complexity, using the multiset extension
of the ordering >-e. The corresponding ordering, which we denote by >-e, is
well-founded. Moreover, if P >-e Q, then u[PO"]p >-e u[QO"]p, for all terms
u, positions in u, and substitutions 0". However, since the complexity of a
proof step depends on the context in which it appears, Q >-e Q' does not
necessarily imply P[Q] >-e P[Q']. Therefore >-e is not a proof ordering.
We will first show that all transformation rules of 'R,e are decreasing
with respect to the above complexity measure. The transformation rules
reflecting orientation, simplification, and elimination of peaks decrease the
complexity of a proof in the first component. The transformations rules re-
flecting collapse reduce the complexity in the second component; the trans-
formations rules reflecting extension reduce it in the second or fourth com-
ponent. Protection and composition reduce the complexity in the fourth
and fifth component, respectively.
i) Extension. We have u[s]p -+~S:=.l.t u[t]p >-e u[s]p -+~[61S:=lu[tl u[t]p
because ({[u[s]p]) , s,.1.,.1., [u[t]p]) >-e ({[u[s]p]},.1.,.1, Ipl, [u[t]p]).
Similarly, if p f. A, then u[s]p -+~S:=lt u[t]p >-e u[s]p -+~[61S:=lu[tl u[t]p
because ({[u[s]p]},.1,.1, Ipl, [u[t]p]) >-e ({[u[s]p]},.1.,.1, 0, [u[t]p]).
ii) Orientation. We have s -+~S:=Tt t >-e s -+~S:=.l.t t because {[s], [t]} >-mul
{[s]}.
iii) Protection. By similar arguments as in the first case of extension.
vi) Deletion. We have s -E t >-e s -A t because {[s], [t]} >-mul ([u]},
for each term u in s -A t.
v) Simplification. We have s -E t >-e s -+RIA u -E t because
{[s], [t]} >-mul {[v]}, for each term v in s -+RIA u, and {[s], [t]} >-mul
{[u], [t]}.
vi) Composition. We have s -+~S:=.l.t t >-e s -+~S:=.l.U u +-RIA t because
({[s]) , s,.1.,.1., [t]) >-e ({[s]) , s,.1,.1, [u]) and in addition s is bigger than
each term in u +-RIA t.
Also, S -+~S:=lt t >-e s -+~S:=lU u +-RIA t because ({[s]},.1,.1,O,[t]) >-e
({[s]},.1,.1., 0, [u]) and s is bigger than each term in u +-RIA t.
vii) Collapse. If s t> v, then s -+~S:=.l.t t >-e s -~p s' -+~s:="w U -~S:=Tt t
because the rewrite step s -+~S:=.l.t t is more complex than all proof steps in
s -A s' -+~s:="w u (in the second component) and also more complex than
u -~S:=Tt t (in the first component).
viii) Peaks. We have s +-R u -+RA t >-e s -A v -E W -A t because u
 THE EXTENDED RULE METHOD 59

is bigger than each term in 8 +-+ Av +-+ E W +-+ At.

viii) Cliffs, non-overlaps. By the same arguments as in the proof of
Theorem 3.12.
ix) Cliffs, variable overlaps. Let P be a variable overlap 8 -~A:lOV U +-+~q
= =
t' -!'A:I"W' t, where q pq'q" and vlq' :1:, for some variable :1:, and either
n = .1 or n = 1. In addition, Vi >- Wi. Let Q be the proof 8 -~A:lOV U and
Q' the proof

so that P = QU[Q/]pq'. Then P can be replaced by a rewrite proof modulo

A of the form pi = PI· .. P"Q"Qm ... Ql, where all proofs Pi and Qi are
of the form u' -RA U" (cf. the proof of Theorem 3.12).
Since the rewrite system RIA is terminating, we have k > o. Then all
terms in the proof P2 ... P"Q"Qm··· Ql are strictly smaller than 8, so that
Q >-e P2 ··· P"Q"Qm ... Ql. In addition, if n = .1 (Le., the rewrite step in
Q' is by application of an unprotected rule), then U[Q/]pq' and PI have the
=
same complexity. On the other hand, if n 1 (i.e., the rewrite step in Q' is
by application of a protected rule), then U[Q/]pq' is the composition of two
= =
proofs Q(1) U +-+~q t' and Q(2) t' -!'A:llW' t. Similarly, the proof PI is
th e composl·t·Ion 0 f t wo proo~s
r. p(l)
1 = <q I
8 +-+:4: 8 an
1
d p(2)
1
,
= q
81 -V'A:llW' 81.
Then p~l) has the same complexity as Q(I) and Q >-e p~2). (The third
component of the complexity ensures that proof steps by protected rules
are simpler than proof steps in A. It would be sufficient to use a constant
instead of (if, but the slightly more complicated complexity measure will
be of advantage in the case of sets A of associativity and commutativity
axioms discussed below.) In either case, we have P >-e pl.
We have now proved that all transformation rules Q => Q' of ne are
decreasing with respect to the given complexity measure. Thus we also
have u[Qu]p >-e u[Q'u]p, for all terms u, positions in u, and substitutions
u. It can be shown that in all the cases under consideration, we also have
P[Q] >-e P[Q/], which implies that ne is terminating. Q.E.D.

We can now characterize (non-failing) derivations that induce normal-

izing sequences of proof transformations.

Lemma 3.20. A non-failing derivation Eo; No; 80 I-e E l ;Nl ;81 I-e ... is
fair with respect to ne and He if the set of critical pairs CPA(Roo ) is a
subset of U" E" and the set of extended rules EXTA(Roo ) is a subset of
U"8,,.
Proof. Let Eo; No; 8 0 I-e E l ; N l ; 8 1 I-e ... be a derivation for which Eoo =
0, CPA(Roo ) is a subset of U" E", and EXTA(Roo) is a subset of U" S".
60 EXTENDED COMPLETION

We have to show that whenever a proof P in AU Eoo U Roo contains a peak

or cliff, then there is a proof Q in AU Ui(Ei URi), such that P ~t Q.
Since Eoo = 0, let us assume P is a proof in A U Roo, but contains a
peak s +-Roo U -(Roo)A t or a cliff s +-A U -(Roo)A t. Any peak or cliff
which is a non-overlap or a variable overlap can be transformed to a rewrite
proof modulo A by ~ t.
If P contains a proper overlap s +-Roo U -(Roo)A t, then by the Ex-
tended Critical Pair Lemma s +-+:A s' +-+CPA(Roo) t' +-+:A t. Since by fairness
CPA(R oo ) ~ UI: EI:, there is a proof s +-+:A S' +-+E. t' +-+:A t, for some k ~ O.
Consequently, there is a suitable proof Q such that P ~ Q. t
Finally, suppose P contains a proper overlap s +-+A U -(Roo)A t. By
fairness, EXTA(Roo) is a subset of Uj Sj, which implies that there is a
proof s -(S.)A t, for some k. Again, we may infer that P ~t Q, for some
proof Q in AU U.(E. URi). Q.E.D.

A completion procedure is said to be fair with respect to extensions if

it generates only derivations for which CPA(Roo ) is a subset of UI: EI: and
EXTA(R oo ) is a subset of UI: SI:. Applying Theorem 2.10 to the inference
system t:, the rewrite system ne, and the set of proofs N e , we obtain:
Theorem 3.21. Let A be a set of equations with a minimal complete unifi-
cation algorithm. If an A-completion procedure is fair with respect to exten-
sions and does not fail for the given input, then (N oo U Soo)A is convergent
modulo A.
Fairness with respect to extensions guarantees the correctness of ex-
tended completion and in this sense characterizes a class of correct comple-
tion procedures. Fair procedures are required (1) to compute all A-critical
pairs between persisting rules and (2) to extend and protect all persisting
rules. Protection of persisting rules may necessitate the computation of
infinitely many extended rules. The requirement can be weakened, though,
for many theories A that are of interest in practice, as we shall demonstrate
for the case of associativity and commutativity.

3.6. Associative-Commutative Completion

By an associative-commutative completion procedure we mean any AC-
completion procedure, where AC is a set of associativity and commutativity
axioms

f(x, f(y, z)) f(f(x, y), z)

f(f(x, y), z) ~ f(x, f(y, z))
f(x,y) ~ f(y, x)
 ASSOCIATIVE-COMMUTATIVE COMPLETION 61

for some operator symbols I (called AC operators). Moreover, we assume

that the ordering ~ (used in the definition of the collapse inference rule)
is defined by: s ~ t if s is equivalent in AC to some term containing an
instance of t, but not vice versa. (This ordering is indeed well-founded.)
The only extended rules with respect to associativity and commutativity
originate from rules I(s, t) -+ u with an AC operator I as outermost symbol
on the left-hand side. They are I(x,/(s,t)) -+ I(x,u) and l(f(s,t),x)-+
I(u,x), where x is a new variable not appearing in s, t, or u.
Unfortunately, extended rules themselves can be extended. For instance,
the extended rule l(x,/(s,t)) -+ I(x,u) spans two further extended rules
I(y, I(x, I(s, t))) -+ I(y, I(x, u)) and l(f(x, I(s, t)), y) -+ l(f(x, u), y). In-
deed, since extended rules cannot be collapsed, no derivation producing a
finite system Roo that contains a rule I(s, t) -+ u can be fair with respect
to extensions. (That is, if Roo = Noo U 8 00 contains a single rule with
left-hand side I(s, t), then it contains rules with arbitrarily large left-hand
sides.) Fortunately, we shall be able to establish the correctness of AC-
completion procedures under considerably weaker requirements.

Definition 3.22. Let R be a rewrite system. We define R e as the rewrite

system consisting of R plus all extensions I(s,x) -+ I(t,x) of rules s -+ t
in R for which there exist no rule u -+ v in R and substitution u, such that
I(s, x) ~AC uu and I(t, x) -+ACUR/AC vu.

The set R e is evidently a subset of RUEXTAc(R). It describes the extended

rules that are actually computed in the Peterson-Stickel procedure.
For example, let R be the set consisting of three rules, x + 0 -+ x,
x + -x -+ 0 and x * 0 -+ O. The set R e consists of R plus a single extended
rule (x + -x) + y -+ 0 + y. The extended rule (x + 0) + y -+ x + y is not in
R e , because it is equivalent under AC to the instance (x + y) + 0 -+ x + y
of x + 0 -+ x. Similarly, since (x * 0) * y ~AC (x * y) * 0 and 0* Y -+R/AC 0,
the extended rule (x * 0) * y -+ 0 * y is not in R e either.

Lemma 3.23. (Re)e = Re, lor every rewrite system R.

Proof. Let s -+ t be a rewrite rule in Re. We show that there exist a

rule u -+ v in R e and a substitution u, such that I(s,x) ~AC uu and
I(t,x) -+ACUR/AC vu.
If s -+ t is a rule in R, then the assertion follows from the definition of
R e • If s -+ t is not in R, it is an extended rule I(S/,y) -+ I(t',y). Let u
be a substitution, such that yu = I(y,x) and zu = z, for all variables z
different from y. Then s'u = s' and t'u = t', so that

I(s,x) = 1(f(S/,y),X) ~AC I(S'u,yU)

62 EXTENDED COMPLETION

and
f(t,x) = f(l(t/,y),X) +-+AC f(t'tT,ytT).
In other words, every extension of an extended rule is equivalent in AG to
an instance of the extended rule itself. Q.E.D.

The essential property of sets R e is expressed in the following lemma

(cf. the notion of "AG-compatibility", Peterson and Stickel 1981).

Lemma 3.24. Let f(s, t) - u be a rule in R for which f is an AG op-

erator. For every term v and substitution tT, there exist terms Vi and w
and a rule s' ~ t' in R e , such that f(l( StT, ttT), v) +-+ AC Vi -~'Rjt' wand
f(utT, v) -::4.CUR/AC w.

Proof. Consider the extended rule f(l(s,t),x) - f(u,x). By the defini-

tion of Re, there exist a rule s' _ t' in Re and a substitution r, such that
f(l(s,t),x) +-+AC sir and f(u,x) -ACUR/AC t'r. We may assume without
loss of generality that XtT is v. Thus, we have f(l(stT,ttT),v) +-+AC (s'r)tT
and f(utT, v) -ACUR/AC (t'r)tT. Since s' - t' is in Re, the assertion follows
immediately. Q.E.D.

Proposition 3.25. Let AG be a set of associativity-commutativity axioms

and Eo; No; So rc AC E1;N1;Sl rc AC .•• be a derivation, such that (i)
=
Eoo 0, (ii) GPAc(Roo) is a subset of U, Ek, and (iii) R~ is a subset of
Uk Sk. Then (Roo)AC is convergent modulo AG.
Proof. Let Eo; No; So rc AC E1;N1;Sl rCAC .•• be a derivation satisfying
the stated conditions. It suffices to show that whenever a proof P in AG U
Roo contains a peak or a cliff (or the inverse thereof), then there is a proof
Q in AG U U(Ej U Rj), such that P >-C Q.
By the same arguments as in Lemma 3.20, it can be shown that when-
ever P contains either a peak or else a cliff which is a non-overlap or a
variable overlap, then there is a suitable proof Q, such that P >-C Q. Sup-
pose P contains a proper overlap s +-+AC U -(R...,)AC t. We may assume
without loss of generality that this cliff pi is of the form

f(l(u,v),w) +-+AC f(u,f(v,w»

+-+AC f( u, f( StT, ttT» -J(.,t)Rj"U' f(u,u'tT)

or

f(v,f(w,u» +-+AC f(l(v,w),u)

+-+AC f(l(stT, ttT), u) - J(.,t)Rj"U' f(u'tT, u),
 ASSOCIATIVE-COMMUTATIVE COMPLETION 63

where f(s,t) ~n u' is a rule in Roo.

By Lemma 3.24, there exist terms Vi and Wi and a rule s' ~ t ' in R~,
such that f(f(sO',tO'),u) +-4 AC Vi -+~'s:=t' Wi and f(u'O',u) -+~cUR~/AC
Wi. In other words, both f(f(u,v),w) and f(v,f(w,u» are reducible by
(R~)AC at the top.
Let us consider one of the two cases, the other is similar. By fairness,
R~ is a subset of UI: SI:, so that the proof

p" = f(f(u,v),w) -+(Roa)AC Wi +-~CU(Roa)IAC f(u,u'O')

is a proof in AC U UI: RI:. We have

f(f(u,v),w) +-4AC f(u,J(v,w» >-e f(f(u,v),w) -+(Roa)AC Wi

(all AC steps in the latter proof are bound on the right) and

f(f(u,v),w) +-4AC f(u,J(v,w» >-e Wi +-~CU(Roa)IAC f(u,u'O')

(all terms in the latter proof are strictly smaller than f(u,J(v,w))). In
sum, there is a suitable proof Q, such that P >-e Q. Q.E.D.

In contrast to Theorem 3.21, the above proposition requires R~, instead

of EXT( Roo), to be a subset of U SI:. The essential point, of course, is that
R~ is finite, whenever Roo is finite.
Let us also point out that AC-critical pairs obtained by superposing on
a proper subterm of an extended rule are superfluous. Namely, if there is
a proper overlap

f( UO', :CO') +- EXTAC(R) f(f(sO', to'), :CO') -+R AC f( v, :c0'),

then there is also a proper overlap uO' +-R f(sO', to') -+RAc v. The former
overlap can be eliminated, if the latter can be eliminated.
The correctness of Peterson and Stickel's associative-commutative com-
pletion procedure follows from Proposition 3.25. A number of convergent
systems have been derived with this procedure (e.g., Hullot 1980).

Example 3.26. Let E be the set of axioms for Abelian groups:

:c+o ~ :c
:c + (-:c) ~ 0
:c+(y+z) ~ (:c+y)+z
:c+y ~ y+:c
64 EXTENDED COMPLETION

and let AG be the set of the associativity and commutativity axioms for +
and R be the set of rules
z+O -+ z
-0 -+ 0
--z -+ z
-(z + y) -+ -z+-y
z+-z -+ 0
(z + -z) +y -+ y

The rewrite system RAG is convergent modulo AG.

Exam.ple 3.27. Augment the above set AG by the associativity and com-
mutativity axioms for *, and augment R by rewrite rules

z*O -+ 0
z*1 -+ z
z*-y -+ -(z * y)
(z * -y) * z -+ -(z * y) * z
z * (y + z) -+ z*y+z*z
(z * (y + z)) * z' -+ (z * y) * z' + (z * z) * z'
Then RAG is an AG-convergent system for associative-commutative rings
with unit.

Exam.ple 3.28. Hsiang (1985) has presented a rewrite system

zE90 -+ z
zE9z -+ 0
zl\O -+ 0
zl\1 -+ x
zl\z -+ z
-z -+ z
x 1\ (y E9 z) -+ zl\yE9zl\z

where E9 (exclusive disjunction) and 1\ (conjunction) are AG operators. The

corresponding system RAG constitutes a convergent system for Boolean
rings.

Termination of associative-commutative rewrite systems can be proved

by polynomial orderings (Lankford 1975, Ben Cherifa and Lescanne 1987)
or by associative path orderings (Bachmair and Plaisted 1985; Bachmair
and Dershowitz 1986). Termination proofs for the above systems can be
found in Peterson and Stickel (1981) and Hsiang (1985).
 THE PROTECTED RULE METHOD 65

3.7. The Protected Rule Method

Jouannaud and Kirchner (1986) described a completion procedure that uses
both extended rules and critical pairs of CPA(R, A). We shall discuss their
approach within our formalism. We assume that the proper subterm order-
ing modulo A is well-founded. (This implies that A contains no equation
t ~ x and, by Lemma 3.11, that the encompassment ordering modulo A is
well-founded.) We denote by J'i the inference system t'~ , with the collapse
rule replaced by the following inference rule:
E;NU{s-d};S 'f s ...... :4:
<p, p
COLLAPSE: 1 S -1/::::InW u,
EU{u~t};N;S
where either p f:. >. or
else s = s' and s t> A V

Let n':r be the proof transformation system obtained from nc by changing

the transformation rules reflecting collapse accordingly. We will further
augment n':r by transformation rules for elimination of cliffs. The Extended
Critical Pair Lemma suggests a transformation rule

for elimination of proper overlaps. The difficulty with this transformation

rule is that when we add it to n':r the resulting proof transformation system
is not terminating. Therefore we shall use a slightly more restrictive version

= =
where (i) v' >- w', v" >- w", (ii) n 1.. or n 1, and (iii) the position q is
strictly below p.
This transformation rule is applicable when an A-critical pair is com-
puted and then oriented, before any simplifications are performed. Thereby
the range of possible simplifications is restricted, as the inference rules of
composition and collapse together are less powerful than simplification of
unoriented equations.
By nj we denote the transformation system n':r, augmented by the
transformation rules for elimination of proper overlaps. The corresponding
transformation relation is denoted by =>:r.

Lemma 3.29. If the proper subterm ordering modulo A is well-founded,

then the transformation system n:r is terminating.

Proof. Let P be a proof

66 EXTENDED COMPLETION

where ei is an equation Ui ~ni Vi. We redefine the complexity of single

proof steps as follows:

({[ti-l], [tin, 1., 1.,1.,1.) ifni=T

({[ti-ln, [ti-ll,,;], f3f, 1., [til) ifni=O
({[ti-ln, [ti-ll,,;], 1., Ui, [tiD if ni = 1. and Hi >- Vi
({[tin, [til,,;], 1., Vi, [ti-1D if ni = 1. and Vi >- Ui
({[ti-ln, 1., Ipi 1,1., [tiD if ni = 1 and Ui >- Vi
({[tin, 1., Ipil, 1., [ti-l]) if ni = 1 and Vi >- Ui
The complexity of a proof is the multiset of all tuples corresponding to its
proof steps.
Complexity tuples are compared lexicographically by the multiset ex-
tension >-mul of the reduction ordering >- (in the first component), the
subterm ordering modulo A (in the second component), the greater-than
relation (in the third component), the standard encompassment ordering
(in the fourth component), and the reduction ordering >- (in the last com-
ponent). We denote this ordering by >-j. Proofs are compared according
to their complexity, using the multiset extension of >-j. We denote this
ordering by >-:r. It is well-founded, if the subterm ordering modulo A is
well-founded, and contains all transformation rules of 1l:r.
The above complexity measure differs from the one used in the proof
of Lemma 3.19 mainly in that proof steps by equations in A have higher
complexity. Most transformation rules can be shown to be decreasing by
similar arguments as in the proof of Lemma 3.19. We consider the remaining
cases in detail.
i) Collapse. Consider the transformation rule
At.......
S -.Si::I.l.t-r
<",S ~tlSi::I"W U +-+USi::lTt
S +-+ji
A t

where S >- t, V >- w, S I>A V, and n = 1. or n = 1. Moreover, either P =/; A

or else S = s'.
If P =/; A, then

(using the first two complexity components).

=
If P A, then S =
s' and s I> v, so that

(using the first four complexity components).

ii) Cliffs, variable overlaps. Let P be a variable overlap s -{;,Si::lOti U +-+~g
= =
t' -!'Si::I"W' t, where q pq'q" and vlg' :1:, for some variable :1:, and either
 THE PROTECTED RULE METHOD 67

n = .L or n = 1. Let Q be the proof 8 +-~AlOV U and Q' the proof

so that P = Qu[Q']'9" As we have shown previously, the variable over-

lap P can be replaced by a rewrite proof modulo A of the form P' =
Pl" ·p"Q"Qm·· ·Q1 (cf. the proof of Lemma 3.19).
Since all terms in the proof Qm ... Q1 are strictly smaller than t, we have
U[Q']'9' ~.7 Qm'" Q1. Furthermore k > 0, so that Q ~.7 Pl'" P"Q".
(Recall that A contains no equations t ~ z. Therefore, all proof steps in
Pl'" PTe apply at positions strictly below p.) We have P ~£ P'.
iii) Cliffs, proper overlaps. Consider a proper overlap

S
~
WAlOV u
<9
+-+1 U
, 9
-V'AI"W'
t

and the corresponding proof

where (i) v' ~ w', v" ~ w", (ii) n =

.L or n =
1, and (iii) the position
q is strictly below p. The proof step s +-+~AlOV u is more complex in the
second component than each proof step in 8 +-+1' s'. It is more complex
than s' -~"AI w" t' in the third component; and more complex than each
proof step in I! +-+A t in the first component.
Finally, in all cases that need to be considered P ~.7 P' also implies
Q[u[PO"],] ~.7 Q[u[P' 0"],]. Q.E.D.
We can now describe (non-failing) derivations that induce normalizing
sequences of proof transformations.
Lemma 3.30. A non-failing derivation Eo; No; So 1-£ E1; N1; Sl 1-£ ... is
fair with respect to'R.7 andN£ if (a) CPA(Roo) is a subset ofU"E", and
(b) for each rule 8 - t in Roo and equation u ~ v in A for which some
non-variable subterm ul, is A-unifiable with 8, either the extended rule
u[s], - u[t], is contained in U" S", or else all A-critical pairs of s - t on
u ~ v at position p are contained in U" RJ:.

Proof. The proof is by induction on ~ j and differs from the proof of

Lemma 3.20 only in the elimination of proper overlaps s +-A u -(Roo)A t.
The given assumptions ensure that each such cliff can be transformed by
~ j to a simpler proof. Q.E.D.
An A-completion procedure is said to be fair if all non-failing derivations
it generates satisfy conditions (a) and (b) in the previous lemma.
Lemmas 3.29 and 3.30 indicate that Theorem 2.10 can be applied to the
inference system :J.
68 EXTENDED COMPLETION

Theorem 3.31. Let A be a set of equations with a minimal complete uni-

fication algorithm, such that the proper subterm ordering modulo A is well-
founded. If an A-completion procedure is fair and does not fail for the given
input, then (Noo U Soo)A is convergent modulo A.
The theorem applies to all sets of equations A for which the proper sub-
term ordering modulo A is well-founded. This excludes, for instance, theo-
ries with identity axioms f(z,e) ~ z, or equipotency axioms f(f(z» ~ z.
Theories containing such axioms can be dealt with by the extended rule
method. The theorem also indicates that A-critical pairs provide an alter-
native to extended rules. The procedure given by Jouannaud and Kirchner
(1986) is fair in our sense, but may on occasion require computation of
extended (or at least protected) rules.
For instance, in the Jouannaud-Kirchner procedure, if in an A-critical
overlap vu +-+A UU -+R A uu[tu] of a rule s -+ t on an equation u ~ v,
the term vu is not reducible by R, then the extended rule u[s] -+ u[t] is
generated instead of the A-critical pair vu ~ uu[tu]. Our definition of
fairness covers A-completion procedures that never generate extended (or
protected) rules. With such procedures it is possible to construct reduced
systems.
An extended rewrite system RA is said to be reduced if, for every rule
s -+ t in R, (i) no proper subterm of s is reducible by RA, (ii) the term s
is not reducible by R \ {s -+ t}, and (iii) t is not reducible by RA.
Let R be the limit of a fair derivation in :fA in which no rules have been
protected and neither composition nor collapse apply to any persisting rule.
Then (i) no right-hand side of any rule in R is reducible by RA (for otherwise
a composition inference could have been applied), (ii) no proper sub term
of a left-hand side is reducible by R A , and (iii) no left-hand side is a proper
instance of another left-hand side (for otherwise a collapse inference could
have been applied). The system R A , though convergent modulo A, need
not be reduced as it may contain two distinct rules s -+ t and u -+ v, such
that s +-+:A uu, for some substitution u. But we can apply the following
proposition (cf. Jouannaud and Kirchner 1986) to obtain a reduced rewrite
system from R.
Proposition 3.32. Let R be a finite rewrite system and A be a set of
equations, such that the proper subterm ordering modulo A is well-founded
and RA is convergent modulo A. Let R' be the system obtained from R by
deleting any rule s -+ t for which there is a rule u -+ v, distinct from s -+ t,
such that s +-+:A uu, for some substitution u. Then R~ is also convergent
modulo A.
The protection rule can be used to allow for a slightly more general
version of the collapse inference rule. Suppose s ~ t is an A-critical pair
 EXTENDED CRlTICAL PAIR CRITERlA 69

in CPA(N,A) and let u -+ v be a rule in R, such that 8 -1 UO", for

some substitution 0". The equation 8 ~ t can be simplified and replaced by

VO" ~ t. However, fairness requires that 8 ~ t be oriented into a rewrite rule

8 -+ t. Since collapse does not allow reduction by RA at the top, the rule
8 -+ t cannot be collapsed. However, instead of adding 8 -+ t as a rule, we
can add the equation VO" ~ t, while at the same time protecting the rule
u -+ v. This inference is reflected by transformation rules

= =
where (i) Vi >- Wi, v" >- w", (ii) n .L or n 1, and (iii) the position q is
strictly below p and pi is below p. This proof transformation is simplifying
with respect to >-:r, as all proof steps in 8 - ~p' 8 ' are bound on the right,
while 8 -~~ov u is not. Therefore, the above correctness result also holds
if we extend the inference system e by a corresponding new inference rule.
Jouannaud and Kirchner (1986) implicitly use this kind of inference. The
disadvantage is that the rule u -+ v has to be protected, which in the
final analysis may increase the number of rules and prevent construction of
reduced systems.
In their completion procedure, Jouannaud and Kirchner also consider
rewrite relations LUNA, where L contains only left-linear rewrite rules,
and combine extended rewriting with standard rewriting in an attempt to
avoid the costly operations of A-matching and A-unification when dealing
with left-linear rules. This refinement can readily be formalized within our
framework. The goal of such a modified completion procedure is to con-
struct a rewrite system R = LUNUS, such that LU(NUS)A is convergent
modulo A. In other words, this means that all proofs can be transformed
to rewrite proofs modulo A in L U (N U S)A. This requires elimination
of cliffs 8 +-L u -A t, where the second proof step is below the first.
Such cliffs correspond to extended rewrite steps 8 +-L A t, but the extended
rewrite system LA is not used. Elimination of such cliffs can be achieved
by standard critical pair computation. The proof transformation relation
=?:r can be extended accordingly; for a brief discussion see Bachmair and
Dershowitz (1989, p. 198).

3.8. Extended Critical Pair Criteria

Just as with standard completion, the efficiency of A-completion can often
be improved by sifting out redundant A-critical pairs. Critical pair criteria
for associative-commutative completion have been discussed by Winkler
70 EXTENDED COMPLETION

(1984), Kiichlin (1986a), and Kapur, Musser, and Narendran (1988). We

shall briefly describe how the concept of blocking (Slagle 1974) can be
adapted to A-completion, for sets A for which the proper subterm ordering
modulo A is well-founded.
A proof step s -~R:ltI t is said to be blocked with respect to R and
A if, for all variables z, the term zu is irreducible by RIA, where u is a
=
substitution, such that sip uu and tip vu. =
For example, if R contains rules -(z + y) - -z + -y and 0 + z - z,
where + is an AC operator, then the rewrite step -«z + 0) + y) - R
-(z + 0) + -y is not blocked with respect to R and AC, because the term
z + 0, which is substituted for z, is reducible by RIAC. Most non-blocked
rewrite steps can be eliminated from proofs.
Let P be a proof step s -~R:I .. tI t, where u is not a variable, and let u
be a substitution, such that sip = uu and tip = vu. Suppose u contains
a variable z that is reducible by RIA, say zu -RIA w. Then P can be
replaced by a proof

where zr = w and yr = yu, if y =F z. If u ~n V is an unprotected rule (i.e.,

n = .i), then P >-.7 Q.
An A-critical overlap s +- R U - RA t is said to be blocked if its first and
last step are blocked; an A-critical overlap s +-+ A U -RA t is blocked if its
last step is blocked. An A-critical pair is blocked if its corresponding A-
critical overlap is. Non-blocked A-critical overlaps that involve unprotected
rules only, define redundant A-critical pairs.
In the case of associative-commutative completion, a restricted form of
blocking can be applied to extended (i.e., protected) rules. For instance,
proof steps J(su, zu) - R J(tu, zu) in which an extended rule J(s, z) -
J(t,z) is applied with a substitution u, such that yu is reducible by RIAC,
for some variable y in s, can be simplified by the above prooftransformation.
Informally, proof steps that "extend" a non-blocked rewrite step su - R tu
are redundant. The "extension variable" z, on the other hand may well be
instantiated by a reducible term.
For example, consider the two rules, a + b - c and (a + a) + (b +
b) - d, where the operator + is associative-commutative. The only AC-
critical pairs are those involving the extended rules, (a + b) + z - c + z
and «a + a) + (b + b)) + z - d + z. They require that the extension
variable z be instantiated by a reducible term. If those AC-critical pairs
are considered redundant, no new equation is generated. However, the
system is not convergent modulo AC, as (a + b) + (a + b) has two different
normal-forms, c + c and d, that are not equivalent with respect to AC.
 EXTENDED CRlTICAL PAIR CRITERIA 71

Summary
We have formalized extended completion as an equational inference system
and have established the correctness of various extended completion proce-
dures. The left-linear rule method proposed by Duet (1980) uses standard
matching and unification, but is limited to left-linear rewrite systems, while
other methods that also apply to non-left-linear rules, require A-matching
and A-unification.
The extended rule method is characterized by the systematic use of ex-
tended rules. We have derived sufficient conditions for its fairness and have
shown that the fairness conditions can be considerably weakened in the
case of associativity and commutativity. Our correctness result covers, for
instance, the associative-commutative completion procedure described by
Peterson and Stickel (1981). More recently, Baird, Peterson, and Wilkerson
(1989) and Jouannaud and Marche (1990) have described completion pro-
cedures for sets A of associativity, commutativity, and identity axioms that
also fall into this general framework. The protected rule method generalizes
the Jouannaud-Kirchner procedure. We have proved its correctness under
the assumption that the proper subterm ordering modulo A is well-founded,
which covers all theories A for which congruence classes are finite.
4. ORDERED COMPLETION

Standard completion fails whenever an equation s ~ t is generated, such

that s and t are irreducible, yet incomparable with respect to the given
reduction ordering. Examples of such unorientable equations are commu-
tativity axioms z·y ~ y·z, as the two terms z . y and y . z are incomparable
with respect to any reduction ordering.
For example, let Eo consist of the equations a ~ b, a ~ e, fb ~ b, and
fa ~ d, and let >- be the lexicographic path ordering corresponding to a
precedence >-p in which a >-p b >-p d and a >-p e >-p d. The derivation
Eo;0 I-c {b~e,fb~b,fb~d};{a--+b}
I-c {b ~ e,b ~ d}; {a --+ b,fb --+ b}
I-c {d~e,fd~d};{a--+d,b--+d}
I-c 0; {a --+ d, b --+ d, e --+ d,fd --+ d}
yields a convergent system, whereas the alternative derivation
Eo; 0 I-c {b ~ e,fb ~ b,fe ~ d}; {a --+ e}
I-c {b ~ e, fb ~ b} ; {a --+ e, f e --+ d}
I-c {b ~ e}; {a --+ e,fb --+ b,fe --+ d}
fails (Dershowitz, Marcus, and Tarlecki 1988).
This example indicates that the order in which inference rules are ap-
plied may determine whether or not an unorientable equation is generated. 1
To avoid failure a completion procedure may have to systematically enumer-
ate all possible derivations, e.g., via backtracking. In some cases, standard
completion is bound to fail even with backtracking. In fact, the method
may fail even when a convergent system does exist and it is supplied with
a suitable reduction ordering.
For example, let Eo be the set of equations
h(-z+z) ~ 0
1 * (z + -z) ~ z + -z
-z+z ~ y+-y
1 It might be argued that in the above example the ordering could be extended so
that band c are comparable. However, one can easily devise a similar example in which
band c are replaced by terms (with variables) that are intrinsically incomparable.

73
74 ORDERED COMPLETION

and Ro = 0. Standard completion fails, regardless of which reduction

ordering is supplied as input! The only inference rule that can possibly be
applied to the above set of equations is orientation, which may result in
two rules

1 * (-z + z) -+ 0
1 * (z + -z) -+ z +-z
(no other orientation is possible). These two rules do not overlap and form
a convergent rewrite system. The third equation is unorientable and both
sides are irreducible by the above two rules. As a consequence, no further
inference rules are applicable. Nonetheless, there exists a convergent system

-z+ z -+ 0
z+ -z -+ 0
1*0 -+ 0

for the given equational theory.

Unorientable equations in which one side contains a variable not oc-
curring in the other side can sometimes be dealt with by introducing new
function symbols, a technique suggested by Knuth and Bendix (1967). Sup-
pose, for instance, that the equation -z + z R:: Y + -y is replaced by two
rules -z + z -+ c and y + -y -+ c, where c is a new (minimal) constant.
Completion would then succeed in constructing a convergent system of four
rules
-z+z -+ c
z+-z -+ c
l*c -+ c
0 -+ c
which represents a conservative extension of the original equational theory
(and hence also provides a decision procedure). But very often this tech-
nique leads to the introduction of ever more new function symbols, and the
above example does indicate an inherent inadequacy of standard comple-
tion. In general, given a reduction ordering >-, a set of equations can be
represented by a convergent rewrite system contained in >- if and only if
every congruence class of +-+ E has a unique minimum element with respect
to >- (Avenhaus 1986).
In this chapter, we shall pursue a different approach for dealing with
unorientable equations, called ordered completion, which is designed to
construct sets of equations that define unique ground normal forms. This
ordered completion method is guaranteed to find a convergent system, if one
exists and the reduction ordering supplied to the procedure satisfies some
 ORDERED COMPLETION 75

reasonable conditions. It requires neither backtracking nor introduction of

new function symbols and is a refutationally complete theorem prover for
equational theories, but has the advantage over paramodulation (Robin-
son and Wos 1969) in that equations can always be kept in fully simplified
form and fewer equational consequences need to be considered, as the or-
dering supplied to the procedure gives some measure of direction to the
prover. The method works with all general purpose orderings that have
been proposed for rewriting, e.g., polynomial interpretations and recursive
path orderings. In the more general context of Horn clauses with equality
it yields an inference system consisting of ordered versions of positive unit
resolution and paramodulation (with simplification).

4.1. Ordered Completion

A convergent rewrite system defines unique normal forms for all terms,
while in many applications, including (refutational) theorem proving, the
uniqueness of ground normal forms may be sufficient. In this section we will
present an inference system, called ordered completion, for the construction
of sets of equations that define unique ground normal forms.
We first refine the notion of rewriting, so that all equations (and not
just rewrite rules) can potentially be used for simplification. For example,
even though the commutativity axiom z . y ~ y . z cannot be oriented with
respect to any reduction ordering, some of its instances may be orientable
(e.g., we have /(z) . z >-lpo z· /(z) for the lexicographic path ordering).

Definition 4.1. We call uu ~ vu an orientable instance (with respect to

a reduction ordering >-) of an equation u ~ v if uu >- vu. By E~ we denote
the set of all orient able instances of equations in E.

Evidently, S -+E)o t if and only if S +-+E t by an equation u ~ v and a

substitution u, such that uu >- vu. In particular, S -+E)o t implies S +-+E t
and S >- t (but not vice versa). By definition, the rewrite relation -+E)o
induced by E~ is terminating. Also note that every instance of an orient able
instance is orientable. Rewrite rules can be thought of as equations all
instances of which are orient able in the same direction.
Definition 4.2. A set of equations E is said to be ground convergent (with
respect to a reduction ordering >-) if for all ground terms sand t with
s +-+:E t, there exists a ground term v, such that s -+:E)o v -E)o t.
A ground convergent system defines unique ground normal forms.
In formulating ordered completion as an equational inference system we
take a different approach than with standard completion and describe the
76 ORDERED COMPLETION

inference rules in terms of a proof ordering. We shall consider arbitrary

sets of labelled equations. (Recall that the label of an equation is either a
non-negative number or one of the symbols T or _L)
Let >- be a reduction ordering. The cost of a single equational proof
step s +-+~= .. " t is defined to be
({s},u,n,t) ifs>-t
{ ({t},u,n,s) ift>-s
({s,t},l.,l.,l.) otherwise.
The complexity of a proof is the multiset of the costs of its proof steps. By
>-c we denote the lexicographic combination of (i) the multiset extension
of the reduction ordering >-, (ii) the encompassment ordering 1:', (iii) the
ordering on labels, and (iv) the reduction ordering >-. The ordering >-c is
used to compare tuples representing the cost of single proof steps; proofs
are compared according to their complexity, using the multiset extension of
>- C. We denote this ordering on proofs by >-0. It is indeed a proof reduction
ordering.
The inference system 0>- (also denoted by 0 if >- is clear from the
context) consists of two inference rules:
E
DEDUCTION:
E U {s R:: n t}
if s +-+E t

E U {s R:: n t}
DELETION: if there is a proof P of
E
s R:: tinE such that
s +-+:= .. t t >-0 P

where E denotes a finite set of (labelled) equations. Inference systems 0>-

are called ordered completion systems.
Ordered completion systems are evidently sound.
LeIIllIla 4.3. Whenever E 1-0 E ' , then the two congruence relations +-+E
and +-+EI are the same.
Moreover, the proof reduction ordering >-0 trivially reflects the inference
system 0>-.
For practical purposes, the inference rules are not needed in the gen-
erality in which we have formulated them above and implementations are
usually based on derived inference rules. Simplification techniques, in par-
ticular, can be described as certain combinations of deduction and deletion
inferences. As a matter of fact, ordered completion generalizes standard
completion, in that all inference rules of standard completion are derived
inference rules of ordered completion.
 ORDERED COMPLETION 77

Lemma 4.4. If E I-c E', then E 1-0 E'.

Proof. The various inference rules of standard completion can be derived
from ordered completion as follows.
Deduction. The inference rule for standard completion is a special case
of the corresponding inference rule of ordered completion.
Orientation. Suppose we have E U {s :::::IT t} I-c E U {s :::::I.L t}, where
s >- t. Then there is a derivation by ordered completion,

E U {s :::::IT t} 1-0 E U {s :::::IT t, s :::::I.L t} 1-0 E U {s :::::I.L t},

where the first inference is by deduction and the second by deletion. (Note
that s ->;~Tt t >-0 s ->;~.Lt t.)
Deletion. Observe that E U {s :::::In s} 1-0 E is a deletion inference by
ordered completion, as the proof s -;~ ... s has greater complexity than
the empty proof.
Simplification. Suppose E U R U {s :::::IT t} I-c E U R U {u :::::IT t} is
a simplification inference in standard completion. Then there is a rewrite
step s ->~~.LW u in R, where v >- w (and hence s >- u). We have u -EUR t,
so that there is a deduction inference

E U R U {s :::::IT t} 1-0 E U R U {s :::::IT t, U:::::lT t}

by ordered completion. Now compare the proof s -;~Tt t with S ->~~.LW

u -~~Tt t. The cost of s -;~Tt t is ({s},s, T,t), if s >- t; ({t},t, T,s),
if t >- s; and ({s,t},.l,.l,.l), otherwise. The cost of s ->~~.LW u is
({s},s,.l,u). The cost ofu -~~Tt t is ({t},t, T,u), ift >- u; ({u},u, T,t),
ifu >- t; and ({u,t},.l,.l,.l), otherwise. Checking all the different cases,
we find that

so that there is a deletion inference,

E U R U {s :::::IT t, u :::::IT t} 1-0 E U R U {u :::::IT t}.

Composition. Suppose we have E U R U {s :::::I.L t} I-c E U R U {s :::::I.L u}

and t ->~~.LW U is a proof step in R, where s >- t and v >- w (and thus
t >- u). There is a deduction inference

E U R U {S:::::l.L t} 1-0 E U R U {S:::::l.L t, S :::::I.L u}.

Furthermore, we have
78 ORDERED COMPLETION

because s >- t >- u implies that ({ s}, s,.1., t) is more complex than both
({s},s,.1.,u) and ({t},v,.1.,u). Thus there is a deletion inference

EURU{s::::::1. t,s::::::1. u}l-o EURU{s::::::1. u}.

Collapse. Finally, let EURU{s::::::1. t} I-c EURU{U::::::T t} be a collapse

inference. Then there is a proof step s --+~~.LW u in R, where v >- w (and
thus s >- u) and s t> v. Moreover, we have s >- t. There is a deduction
inference
E U R U {s ::::::1. t} 1-0 E U R U {s ::::::1. t, u::::::T t}
by ordered completion. Moreover,

because s >- u and s t> v imply that ({ s}, s,.1., t) is more complex than
both ({s},v,.1.,u) and ({u,t},.1.,.1.,.1.) (and the cost of u +-+~~Tt t is at
most ({ u, t},.1.,.1., .1.)). Consequently there is a deletion inference

E U R U {s ::::::1. t, u ::::::T t} 1-0 E U R U {u ::::::T t}

by ordered completion. Q.E.D.

Definition 4.5. An ordered completion procedure is a program that takes

as input a set of equations Eo and a reduction ordering >-, and uses the
inference rules of (?-r to generate derivations from Eo. Such a procedure is
said to succeed for a set of equations Eo and a reduction ordering >- if Eoo
is ground convergent with respect to >-.

Consider, for example, an en tropic groupoid defined by the two axioms

(x· y) . (z . w) :::::: (x. z) . (y. w)

(x· y) . x :::::: x.
The first equation is permutative and cannot be oriented in any reduction
ordering. Standard completion will fail for this set of equations, whereas
with ordered completion we can obtain a set of equations

(x·y)·z:::::: (x·w)·z
(x· y) . x --+ x
x . (y . z) --+ x· z
«x·y)·z)·w --+ x·w
(Hsiang and Rusinowitch 1987), which is ground convergent with respect to
the lexicographic path ordering. (Orientable equations are written as rules.)
 ORDERED COMPLETION 79

The set E therefore provides a decision procedure for the word problem in
the above theory. Pedersen (1984) has designed another decision procedure
based on a certain notion of extended rewriting.
We shall next derive sufficient conditions for the success of ordered com-
pletion.
Definition 4.6. A reduction ordering >- is said to be complete (with re-
spect to E) if, whenever sand t are distinct ground terms (with s +-+:8 t),
then either s >- t or t >- s. An ordering is called completable if it can be
extended to a complete reduction ordering.
Complete ordering are thus total on ground terms. We also say more specif-
ically that >- can be completed to > if > is a complete reduction ordering
containing >-.
By a ground rewrite proof (with respect to >-) in E we mean a proof
of the form s -:81- v -:81- t. By definition, a set of equations E is ground
convergent if and only if there exists a ground rewrite proof for every equa-
tion between ground terms that is provable in E. If the reduction ordering
>- is complete, then each proof step s +-+E t, where s i= t, is of the form
s -EI- tor s -EI- t. Thus, a ground rewrite proof with respect to a com-
plete reduction ordering >- is simply a (ground) proof containing no peak
s -EI- U -EI- t. Proof normalization corresponds to elimination of peaks
s -EI- U -EI- t, and can be achieved by computation of suitable critical
pairs.
Definition 4.7. Let s ~ t and U ~ v be two equations with no variables
in common (the variables in one equation are renamed, if necessary) and
suppose some non-variable subterm sip of s is unifiable with u, U being the
most general unifier. We say that the superposition of u ~ v on s ~ t at
position p determines an ordered critical pair tu ~ su[vu]p (with respect to
the ordering >-) if there exists a (ground) substitution T, such that SUT >-
tUT and UUT >- VUT.

As before, the proof tu -~~. SU -~~tI su[vu]p is called a critical overlap;

the term SU, the overlapped term; and the position p, the critical pair
position. By CP>-(E) we denote the set of all ordered critical pairs (with
respect to >-) between equations in E U E-l .
For example, the two equations (x· y) . (z . w) ~ (x . z) . (y . w) and
(x· y). x ~ x overlap in «u· v)· u)· (v' ·v) +-+E «u ·v)· v')· (u ·v) +-+E U· v
and define an ordered critical pair «u· v) . u) . (v' . v) ~ U • v with respect
to the lexicographic path ordering.
An ordered critical pair of an equation on itself at the top need not be
trivial. For instance, superposing the equation x . a ~ a- on itself at the
top may yield a non-trivial equation x . a ~ y . a.
80 ORDERED COMPLETION

The computation of ordered critical pairs with respect to a reduction

ordering >- requires that one decide, given terms s, t, U, and v, whether
there exists a ground substitution u, such that su >- tu and uu >- vu. This
question is decidable, for instance, for lexicographic path orderings based
on a total precedence (Comon 1990). If such inequations cannot be solved
for a given ordering >-, then completion may have to deduce more equations
than are actually necessary to ensure fairness. In any case, computation
of standard critical pairs suffices for fairness, as the set of ordered critical
pairs CP>-(E) is a subset of CP(E U E-l).
The Critical Pair Lemma 2.13 can be adapted to ordered critical pairs
without much difficulty.
Lemma 4.8. (Ordered Critical Pair Lemma, Lankford 1975) Let >- be a
complete reduction ordering with respect to E. For all ground terms s,
t, and U with s +-E>- U -+E>- t, there either exists a ground term v, such
that s -+E>- v +-E>- t, or else s +-+CP>-(E) t.

Proof. The proof is similar to the proof of the Critical Pair Lemma. Non-
overlaps and proper overlaps, in particular, can be dealt with in the same
way. The only difference is in the variable overlap case, where the fact that
>- is a complete reduction ordering is needed to obtain a ground rewrite
proof in E>-. More precisely, any variable overlap s +- E>- U -+E>- t can
be replaced by a proof of the form s -+E>- v +-+E w +-E>- t (cf. the proof
of the Critical Pair Lemma). This proof is a ground rewrite proof, as the
completeness of >- implies that the proof step v +-+ E w is either of the form
v -+E>- w or v +-E>- w. Q.E.D.

The lemma suggests the following notion offairness for ordered completion.

Definition 4.9. A derivation Eo 1-0>- El 1-0>- ... is said to be fair if for

every ground proof P of the form s +-E~ U -+E~ t, there exists a proof Q
of s ~ tin Ui Ei, such that P >-0 Q.
Observe that whenever P is a proof s +-E>- U -+E>- t and Q a corresponding
rewrite proof s -+E>- v +-E>- t, then P >-0 Q. Computation of ordered
critical pairs between persisting equations ensures fairness.
Lemma 4.10. Let >- be a complete reduction ordering with respect to E.
A derivation by ordered completion from the initial set E is fair if the set of
ordered critical pairs CP>-(Eoo) is a subset of the set of all derived equations
UJ;EJ;.
The completeness of the given reduction ordering can also be used to
advantage, as suggested by Martin and Nipkow (1990). For example, let E
 ORDERED COMPLETION 81

consist of the equations

(z . y) . z ~ z· (y . z)
z·y ~ y·x
x . (y . z) ~ y. (x· z)

and let >- be the lexicographic path ordering (which is complete in this
case, as shown below). Then

z . (z . y) +-+ E (x . y) . z +-+ EX' (y . z)

is a critical overlap. Fairness requires that every ground instance

of this critical overlap can be replaced by a simpler proof. Since the ordering
>- is complete, all ground terms are comparable. This additional knowledge
may be exploited in constructing simpler proofs for the various ground
instances of a given peak. For example, if s >- u >- t, then there exists a
ground rewrite proof

u· (s· t) -+E>- U· (t· s) -+E>- t . (u·s) +-E>- t· (s· u) +-E>- s· (t. u).

On the other hand, if s = u and u >- t, then the peak can be replaced by a
one-step proof
S·(S·t)-+E>- s·(t·s).
The above set of equations actually forms a ground convergent system for
associative-commutative operators with respect to the lexicographic order-
ing (Martin and Nipkow 1990).
Fair derivations always succeed:
Theorem 4.11. Let >- be a complete reduction ordering with respect to E
and let Eoo be the limit of a fair derivation from E by the ordered completion
system 0>-. Then Eoo is ground convergent with respect to >-.

Proof. Let Eo 1-0>- El 1-0>- ... be a fair derivation and >- be a complete
reduction ordering with respect to Eo. We will show that for every ground
proof P of s ~ t in Ui Ei, there exists a ground rewrite proof Q of s ~ t in
E oo , such that P to Q.
Suppose the assertion is not true. Then there exists some ground proof
in Ui Ei which is minimal with respect to the proof ordering >-0 but is
not a ground rewrite proof. Let P be a minimal such proof. Since the
proof ordering >-0 reflects ordered completion, P has to be a proof in Eoo.
82 ORDERED COMPLETION

Using the fact that the reduction ordering >- is complete and P is a minimal
non-rewrite proof of s ~ t, we may infer that P actually has to be a peak
s <-E>- U -E>- t. But this contradicts the fairness assumption, which
states that no peak in E~ is a minimal proof. Q.E.D.

The theorem applies to complete reduction orderings. If a precedence or-

dering on function symbols is total, then it can be extended to a complete
reduction ordering on terms by way of a lexicographic path ordering. In
other words, lexicographic path orderings are completable.

Lemma 4.12. Let >-p be a total precedence ordering on function symbols.

Then the corresponding lexicographic path ordering >- is complete.

Proof. Suppose the lexicographic path ordering ordering >- is not com-
plete. Let s =
f(sl, ... ,sm) and t =
g(t1, ... ,tn ) be two distinct ground
terms of minimal combined size, such that neither s >- t nor t >- s.
Then the term s has to be comparable with all subterms ti of t, and
t has to be comparable with all subterms Sj of s. In fact, we must have
s >- ti, for all i with 1 ::; i ::; n, for otherwise t >- s. By the same argument,
t >- Si, for all i with 1 ::; i ::; m. But then f >-p 9 would imply s >- t, and
9 >-p f would imply t >- s. Since >-p is total, the two symbols f and 9 have
to be identical.
Since sand t are distinct, we know that there exists an i with 1 ::; i ::; m,
such that Si # ti, while Sj = tj, for all j with j < i. The two terms Si and
ti must be comparable. Yet Si >- ti implies S >- t and tt >- Si implies t >- s,
either of which contradicts the assumption that sand t are incomparable
with respect to >-. Q.E.D.

All general-purpose term orderings used in practice are completable. For

instance, any ordering based on polynomial interpretations (Lankford 1975,
1979) can be extended to a complete ordering by combining it with a well-
founded ordering to distinguish ground terms having the same interpreta-
tions.
Ordered completion is sound in that its inference rules preserve the given
equational theory. If one is primarily interested in the ground equational
theory, i.e., the set of all ground equations s ~ t for which s +-+E t, then
the following inference rules, which preserve only the ground theory, may
 ORDERED COMPLETION 83

be used for the construction of ground convergent systems:

E
DEDUCTION: if su +-+E tu for every ground
substitution u

EU{s~nt}
DELETION: if, for every ground substitu-
E
tion u, there exists a proof P
of su ~ tu in E such that
su +-+:R$"t tu >-0 P

A specific inference system consisting of inference rules derived from these

deduction and deletion rules has been described by Martin and Nipkow
(1990).
A number of ground convergent systems, including the examples below,
have been described by Martin and Nipkow (1990) and Peterson (1990).

Example 4.13. The ground theory of an idempotent, associative, commu-

tative binary operator can be represented by the set of equations

(x· y) . z ..... x . (y . z)
x·y ~ y·x
x . (y . z) ~ y . (x . z)
x·x ..... x
x· (x· y) ..... x·y

which is ground convergent with respect to the lexicographic path ordering.

Example 4.14. Abelian groups. The set of equations

x+O ..... x x + (-x) ..... 0

O+x ..... x x+ (-x+y) ..... y
x+y ~ y+x -(x + y) ..... -x+-y
(x+y)+z ..... x + (y + z) --x ..... x
x+(y+z) ~ y+(x+z) -0 ..... 0

is ground convergent with respect to the lexicographic path ordering >-lpo

corresponding to a precedence >- in which - >- + >- O. (Orientable equa-
tions are written as rules.) The reader may want to compare this ground
convergent system with the AC-convergent rewrite system given in the pre-
ceding chapter.
84 ORDERED COMPLETION

Example 4.15. Boolean rings. The set of equations

x$O -+ x xAO -+ 0
O$x -+ x OAx -+ 0
xAI -+ x
lAx -+ x
x$x -+ 0 xAx -+ x
x$y ~ y$x xAy ~ yAx
(x$y)$z -+ x$(y$ z) (x Ay) A z -+ xA(yAz)
x $ (x $ y) -+ y xA(xAy) -+ xAy
x$(y$z) ~ y$ (x $ z) xA(yAz) ~ yA(xAz)
xA(y$z) -+ (x Ay) $ (x $ z)
(x$Y)Az -+ (xAz)$(YAz)

is ground convergent with respect to the lexicographic path ordering >-'po

corresponding to a precedence >- in which A >- $ >- I >- O. A rewrite system
for Boolean rings which is convergent modulo associativity and commuta-
tivity has been described in the preceding chapter.

4.2. Construction of Convergent Rewrite Systems

Ordered completion has been designed to allow the construction of ground
convergent sets of equations. In most cases of practical interest, ordered
completion will actually succeed in constructing a convergent rewrite sys-
tem for a given equational theory, provided such a rewrite system exists at
all and the given reduction ordering is completable.
The results in this section apply to a specific version of ordered comple-
tion, which we call unfailing completion. By U>- we denote the standard
completion system C>- augmented by the following inference rule:
E;R
DEDUCTION: if S +-+E U +-+E t, s !t U,
EU{s ~T t};R
and t !t U

Inference systems U>- are called unfailing completion systems. (As before,
we write E; R to denote a set of equations E U R, where E consists of
equations s ~T t and R of equations S~.L t.)
Unfailing completion applies not just to complete orderings, but also
to completable orderings. This greater flexibility in regard to the ordering
comes at the expense of a weaker fairness condition which may require
computation of more critical pairs.
Definition 4.16. Let s ~ t and U ~ v be two equations with no variables
in common, where some non-variable subterm sip of s is unifiable with u,
 CONSTRUCTION OF CONVERGENT REWRITE SYSTEMS 85

u being the most general unifier. We say that the superposition of 11. ~ V
on s ~ t at position p determines a semi-critical pair tu ~ su[vu]p (with
respect to the ordering >-) if tu ~ su and vu ~ uu.
By S p~ (E) we denote the set of all critical pairs with respect to >- between
equations in E U E- 1 • It is evident from the definitions that every ordered
critical pair is a semi-critical pair, but not vice versa. In other words,
CP~(E) ~ SP~(E).

Definition 4.17. A derivation in the unfailing completion system u~ is

said to be fair if the set of semi-critical pairs SP~(Eoo U Roo) is a subset
of Ui(Ei U R;).

Proposition 4.18. Let> be any complete reduction ordering (with respect

to E) containing >-. If a derivation from E by the unfailing completion sys-
tem u~ is fair, then the corresponding limit Eoo U Roo is ground convergent
with respect to >.

Proof. The proof is similar to the proof of Theorem 4.11. Observe that
C P> (Eoo U Roo) is a subset of S P~ (Eoo U Roo) and that any non-deduction
inference by u~ is also an inference by U> . Q.E.D.

Let :F and V be given sets of function symbols and variables, respec-

tively, and let /C be a set of constants disjoint from:F. Any reduction
ordering >- on 7(:F, V) can be extended to a reduction ordering >-~ on
7(:F U /C, V) as follows.
Let c be any minimal (with respect to >-) constant of :F and let /{J be
the mapping from 7(:F U /C, V) to 7(:F, V) for which /{J(t) is the result
of replacing in t every constant of /C by c. Moreover, let >-Ipo be the
lexicographic path ordering based on some total precedence ordering on
:F U /C. We define, for all terms sand t in 7(:F U /C, V): 8 >-~ t if either
/{J(8) >- /{J(t), or else /{J(8) = /{J(t) and 8 >-Ipo t.

Lemma 4.19. Let>- be a reduction ordering on 7(:F, V) and let >-~ be as

described above.
(1) The binary relation >-~ is a reduction ordering.
(2) The restriction of>-~ to terms in 7(:F, V) coincides with >-.
(3) Let E be any 8et of equations, such that 8 +-+E t implies /{J(8) +-+E
/{J(t), for all ground terms 8 and t in 7(:F U /C). Then >-~ is complete with
respect to E if and only if>- is complete with respect to E.

Proof. (1) The relation >-~ can easily be shown to be transitive and ir-
reflexive. It is also well-founded. For suppose there is an infinite sequence
tl >-~ t2 >-~ ... of terms in 7(:F U /C, V). Then there is a corresponding
86 ORDERED COMPLETION

sequence cp(td t CP(t2) t ... of terms in T(:F, V). Since >- is well-founded,
we have cp(tj) = cp(ti+l) = ... for some j. But then there is an infinite se-
quence cp(tj) >-lpo cp(ti+d >-lpo . .. which contradicts the well-foundedness
of the lexicographic path ordering. We conclude that >-A: is a well-founded
ordering. It is also a rewrite relation.
Let s and t be arbitrary terms for which s >-A: t. We will show that
u[su]p >-A: u[tu]p, for all terms u, position p in u, and substitutions u. First
note that s >-A: t implies cp(s) t cp(t). Thus

where zu' = cp(zu) , for all variables z. If cp(s) >- cp(t), then obviously
cp(u[su]p) >- cp(u[tu]p), and therefore u[su]p >-A: u[tu]p. On the other hand,
if cp(s) = cp(t) then cp(u[su]p) = cp(u[tu]p). But also s hpo t, and hence
u[su]p >-lpo u[tu]p, so that again u[su]p >-A: u[tu]p. We conclude that >-A: is
a reduction ordering.
(2) Follows immediately from the definition of >-A:.
(3) Let E be a set of equations, such that s +-+E t implies cp(s) +-+E cp(t),
for all ground terms sand t in T(:F U .q.
If >-A: is complete with respect to E, then any two distinct ground terms
sand t in T(:F), for which s +-+:E t, are comparable with respect to >-A:.
Using (2) we infer that s and t are also comparable with respect to >-.
On the other hand, suppose >- is complete with respect to E. Let
sand t be any two distinct ground terms in T(:F U 1::) with s +-+e t.
Then cp(s) +-+e cp(t) and, since >- is complete with respect to E, either
=
cp(s) >- cp(t), or cp(t) >- cp(s), or cp(t) cp(s). Furthermore, either s hpo t
or t >-lpo s, as the lexicographic path ordering is complete. Therefore, we
have either s >-A: t or t >-A: s, whenever s and t are distinct. Q.E.D.

Two sets of equations E and E' are said to be literally similar if each
equation s ~ t in E is literally similar to an equation u ~ v in E', and vice
versa. Recall that if a rewrite system R is reduced, then no right-hand side
of a rule in R and no term encompassed by a left-hand side of a rule in R
is reducible by R.

Theorem 4.20. Let R be a reduced convergent system for E and>- be a

completable (with respect to E) reduction ordering containing R. If Eoo U
Roo is the limit of a fair and simplifying derivation from E by the unfailing
completion system U~, then Eoo = 0 and Roo is literally similar to R.

Proof. Let :F and V be the given sets of function symbols and variables,
respectively. In addition, let I:: be a set of new (Skolem) constants, which
contains a unique constant z for each variable z in V and an additional
 CONSTRUCTION OF CONVERGENT REWRITE SYSTEMS 87

constant c not associated with any variable. Let >- be the given reduction
ordering. By our assumption, the ordering >- can be extended to a reduction
ordering> on T{:F, V) that is complete with respect to E. The ordering
> in turn can be extended to a reduction ordering >IC on T{:F U K, V)
that is also complete with respect to E. (Observe that 8 +-+E t implies
<p(8) +-+E <p{t), for all ground terms 8 and tin T(:FUK).) We may assume,
without loss of generality, that the constant c is minimal with respect to
>-IC .
By i we denote the result of replacing in t all variables by their corre-
sponding Skolem constants. Note that a term t is irreducible by R if and
only if its Skolemized version i is irreducible by R. Furthermore, as the
ordering >IC contains R, a term in T(:F U K, V) is irreducible if and only if
it is minimal (with respect to >IC) in its congruence class.
Let now Eoo ; Roo be the limit of a fair and simplifying derivation from
E ; 0. We first show that all left-hand sides of R are reducible by Roo. If
8 - t is a rewrite rule in R, then S +-+Eoo i, so that by Proposition 4.18,
there exists a ground rewrite proof of S ~ i in E"&,/C U R"&,/C. The term
i is irreducible by R and therefore minimal in its congruence class. As
a consequence, any ground rewrite proof of s ~ i has to be of the form
s -~>/CUR>/C i.
Let P be one such proof that is minimal with respect to the proof
ordering induced by > IC. If the first proof step of P is by a rule in Roo,
then s (and hence 8) is reducible by Roo, and we are done. Let us therefore
assume that the first proof step is by an equation in Eoo. Since all proper
sub terms of s are irreducible by R, and therefore minimal in their respective
congruence classes, the first proof step in P must be of the form s +-+~l'::jtl w.
(That is, the equation u ~ v applies at the top.) This implies that sand
8 are instances of u. All proper instances of 8 are irreducible, and hence
minimal in their congruence class. Thus, if 8 were a proper instance of u,
then u would be irreducible by R and v >- u, which contradicts s >IC w. In
short, 8 and u have to be literally similar.
Since u ~ v is an equation in Eoo (and the corresponding derivation is
simplifying), the two terms u and v are incomparable with respect to >-, so
that u 't. v. Thus P must contain at least two proof steps. Let

be the first two proof steps in P and and let u be a substitution, such that
= =
s uu and w vu. Since the first proof step applies at the top, the proof
Q is a variable or a proper overlap. A variable overlap can be ruled out, as
xu is irreducible for all variables x occurring in u or v. (If x occurs in u,
then xu is a constant in K, and hence is irreducible; if x occurs in v, but
88 ORDERED COMPLETION

not in u, then xu = c because of the minimality of the proof P.) Suppose

Q is a proper overlap.
Let u' be a substitution, such that for all variables x occurring in v but
not in u, xu' = z, where z is a variable occurring neither in u nor in Vi and
= =
yu' y, otherwise. Then uu' u and there exists a proof

which is a critical overlap with respect to >- (i.e., u ~ vu' and v'r' ~
u'r') and hence determines a semi-critical pair u ~ vu'[v'T']p. (Here r' is
such that u'r'p = u'r and v'r'p = v'r, for some substitution p.) Since
(u'r)p' >JC (v'r)p', for some substitution p', we clearly have v'r ~ u'r. On
the other hand, if vu' = v, then u ~ VU'i and if vu' ::I v, then v contains
some variable not occurring in u, so that again u ~ vu'. Thus u ~ vu' [v' r']p
is indeed a semi-critical pair of Eoo U Roo. The proof

is less complex than Q, which contradicts that P is a minimal proof of

S ~ i. In short, u ~ v cannot be an equation in E oo , but has to be a rule
in Roo.
We have thus shown that all left-hand sides of R are reducible by Roo,
from which we may easily infer that Eoo =0 and that R is literally the
same as Roo. Q.E.D.

The above theorem applies to completable reduction orderings. Reduction

orderings induced by reduced convergent rewrite systems need not be com-
pletable, however. For example, the rewrite system R, consisting of rules
f(h(x» ~ f(i(x», g(i(x» ~ g(h(x», h(a) -+ c, and i(a) -+ c, is reduced
and convergent. Any complete reduction ordering> for R must be such
that h(a) > i(a) or i(a) > h(a). If h(a) > i(a), then g(h(a» > g(i(a»i
while from the second rule in R we infer g(i(a» > g(h(a». A similar
contradiction can be derived from the assumption i(a) > h(a).
Devie (1990) has proved a result similar to the above theorem which
requires not that the given ordering be completable, but instead that R be
a set of linear equations. We next characterize a class of rewrite systems R
for which the rewrite relation -+R is completable (with respect to R).
A reduction sequence (of length n) in R is any proof of the form to -+ R
tl ~R ... -+R tn. If R is finite and terminating, then (by Konig's Lemma)
there are only finitely many reduction sequences with fixed initial term t.
A reduction sequence to ~: tl ... -+~::: t n - l ~: tn is called innermost
if, for all i with 1 :5 i :5 n, each proper subterm of ti-Ilp; is irreducible
by R. We denote by I(t) the length of the shortest innermost reduction
 CONSTRUCTION OF CONVERGENT REWRITE SYSTEMS 89

sequence from t to a normal form t'. If >- is a complete reduction ordering

with respect to R (but does not necessarily extend R), then we define the
=
ordering >-k by: s >-k t if s ...... Rt and either I(s) > I(t) or else I(s) I(t)
and s >- t.
Lemma 4.21. If R is a reduced convergent system, then the ordering >-k
contains R and whenever s >-k
t, then u[s]p >-k
u[t]p, for all terms s, t,
and u, and positions p in u.

Proof. If R is reduced, then I(s) = 1 and I(t) = 0, for every rule s -+ t

in R. Hence, >-k contains R. Now suppose that s >-k t, and let s' be the
(unique) normal form of sand t in R. Any shortest innermost reduction
sequence from u[s] can be rearranged so that s is reduced to s' before
any other rewrite steps are applied. In other words, there is a shortest
innermost sequence of the form u[s] -+R u[s'] -+R u'. Since there exists a
corresponding innermost sequence u[t] -+ R u[s'] -+ R u', we conclude that
I(u[s]) 2: I(u[t]), and consequently u[s] >-k u[t]. Q.E.D.

The ordering >-kneed not be a rewrite relation. For example, if R is

{f(x) -+ g(x,x,x),a b}, then f(x) >-k g(x,x,x), but f(a) ik g(a,a,a).
-+
But the restriction of >-k to ground terms is a rewrite relation.
A term s is said to overlap another term t if it can be unified with some
term literally similar to a non-variable sub term of t.
Proposition 4.22. If R is a reduced convergent rewrite system wherein no
variable appears more often in a right-hand side than in the corresponding
left-hand side and no left-hand side overlaps any right-hand side, then the
reduction ordering -+ ~ is completable.

Proof. Let >- be the transitive closure of the union of the reduction or-
dering -+~ and the restriction of >-k to ground terms. We claim that this
ordering is a well-founded rewrite relation.
To prove well-foundedness, we first show that su >-k tu, for every
ground instance su -+ tu of a rule in R. Let us denote by u' the substitu-
tion that maps each variable x to the normal form of xu. Since no variable
appears more often in a right-hand side of a rule than in the corresponding
left-hand side, no shortest innermost reduction sequence tu -+R ... -+R tu'
can be longer than a shortest innermost sequence su -+ R ... -+ R su'.
Since no left-hand side of R overlaps any right-hand side, the term tu' is ir-
reducible in R, whereas su' is reducible. Thus I(su) > I(tu), which implies
su >-k tu.
In sum, we have proved that s -+R t implies s >-k t, for all ground terms
sand t. Consequently, the ordering >- is terminating on ground terms, and
hence well-founded. Q.E.D.
90 ORDERED COMPLETION

As an immediate corollary we obtain:

Corollary 4.23. (Dershowitz and Marcus 1985) If a ground rewrite sys-

tem is convergent and reduced, then it is contained in some complete reduc-
tion ordering.

4.3. Refutational Theorem Proving

Standard completion is primarily a tool for constructing convergent rewrite
systems, but has also been used as an equational theorem prover. In this
regard the possibility of failure is detrimental, as provability in equational
theories is semi-decidable. Ordered completion, on the other hand, is refu-
tationally complete for equational theories, and hence provides a semi-
decision procedure for the provability problem.
Let :F be a given set of function symbols, V be a given set of variables,
and E be a set of equations between terms in T(:F, V). Suppose we want
to check whether an equation s ~ t is provable in E. Take the Skolemized
version S ~ i of s ~ t (i.e., s and i are obtained from sand t, respectively,
by replacing each variable by a unique Skolem constant) and let >- be a
complete reduction ordering on T(:F uK-, V), where K- is the set of Skolem
constants occurring in s and i. If Eoo is the limit of any fair derivation by
the ordered completion system O~ from the initial set E, then Eoo is ground
convergent with respect to >-. Now, if s ~ t is provable in E, then s ~ i is
also provable in E and hence there exists a ground rewrite proof of s ~ i in
E~. Conversely, if s ~ i is provable in Eoo, then s ~ t is provable in E. In
short, s ~ t is provable if and only if the two Skolemized terms sand i can
be rewritten to a common normal form by E~. Ordered completion thus
provides a semi-decision procedure for the provability problem in equational
theories.
Superposition, which forms the basis for critical pair computations, is es-
sentially an ordered version of paramodulation (Robinson and Wos 1969).
Ordered completion also uses the given reduction ordering to determine
which equations are redundant and can be deleted. In practice, deduction
and deletion are combined in various ways, to allow for simplification of
equations (via normalization of terms). Systematic simplification may con-
siderably reduce the search space of a proof procedure, without destroying
refutation completeness.
The idea of extending standard completion by computing equational
consequences of unorientable equations can be traced back to the work of
Brown (1975) and Lankford (1975) on integrating resolution and simplifi-
cation by rewriting (for general first-order clauses with equality). Peterson
(1983) proved the refutation completeness of an inference system comb in-
 HORN CLAUSES WITH EQUALITY 91

ing resolution, paramodulation, and simplification with respect to orderings

isomorphic to w on ground terms. (This class of orderings excludes many
important orderings, such as most path orderings.) A similar inference sys-
tem for more general orderings, but without simplification, has been con-
sidered by Hsiang and Rusinowitch (1986). Further results in this direction
have been obtained by Bachmair and Ganzinger (1990a, b) and Rusinow-
itch (1991). Fribourg (1985) proved the completeness of a restricted version
of paramodulation with locking resolution.
Hsiang and Rusinowitch (1987) used transfinite semantic trees to prove
the refutation completeness of an unfailing completion procedure, with
a simplification rule that is (due to the structure of transfinite semantic
trees) based on the subterm ordering, rather than on the encompassment
ordering.2
Implementations of unfailing completion have been reported by Mzali
(1986) and Ohsuga and Sakai (1986). Anantharaman, Hsiang, and Mzali
(1989) have implemented a procedure that combines unfailing completion
with associative-commutative completion. Experiments with this prover
have been described by Anantharaman and Hsiang (1990).

4.4. Horn Clauses with Equality

Ordered completion, as a technique for constructing ground convergent sets
of equations, can be applied to the more general context of Horn clauses
with equality. We will show that the combination of ordered completion
with an ordered version of unit resolution is a refutationally complete the-
orem proving method for such clauses.
Let :F and V be given sets of function symbols and variables, respec-
tively. In addition, let P be a set of predicate symbols, disjoint from :F
and V. We assume that P contains the binary symbol ~ (which denotes
equality). .
By an atomic formula (or an atom) we mean an expression P(tl, ... , tn),
where t 1 , ... , tn are terms in T(:F, V) and P is an n-ary predicate symbol
in P. Atomic formulas with the equality predicate are written in infix
notation s ~ t and called equality atoms. The set of ground atoms is called
the Herbrand base; the set of ground terms T(:F), the Herbrand universe.
A clause is a pair of multisets of literals, usually written r - a. The
multiset r is called the antecedent; the multiset a, the succedent. The
letters A and B are used to denote atoms; the letters C and D, to denote
2Subtenn-based simplification is too weak for practical purposes. In particular, sim-
plification of one side of an equation at the top is not always possible in the procedure
proposed by Hsiang and Rusinowitch. For example, the equation (x. y) . (y- . z) ~ x· z
cannot be simplified by the rule x· (y. z) ..... (x. y) . z.
92 ORDERED COMPLETION

clauses. We usually write r ll r 2 instead of r l U r 2 ; r,A or A,r instead

of r U {A}; and At, ... ,Am -+ B I , ... ,Bn instead of {AI, ... , Am} -+
{B I , ... ,Bn}. A clause AI, ... ,Am -+ B I , ... , Bn represents an implication
Al A· .. A Am :::) BI V ... V Bm. The empty clause indicates a contradiction.
Clauses of the form r, A -+ ~,A are called tautologies.
A clause is called a Horn clause if its succedent contains at most one
atom. A unit clause is a clause in which antecedent and succedent combined
contain only one atom. We speak of a positive unit clause, if that atom
occurs in the succedent.

Definition 4.24. An (Herbrand) interpretation is a subset of the Herbrand

base. An interpretation I is said to satisfy a ground clause r -+ ~ if either
r Cf:. I or else ~ n I 1: 0. It satisfies a (non-ground) clause r -+ ~ if it
satisfies all ground instances ru -+ ~u.

We also say that a clause C is true in I, if I satisfies C; and that C is false

in I, otherwise. For instance, a tautology is satisfied by any interpretation.
Clauses which are satisfied by no interpretation are called unsatisfiable.
The empty clause, for instance, is unsatisfiable. If I satisfies all clauses of
a set N, we say that I is a (Herbrand) model of N. A set of clauses is
unsatisfiable if it has no model. We also write C 1 , ... ,Cn 1= C to indicate
that C is true in every (Herbrand) model of {C1 , ... , Cn }.
We are mainly interested in equality interpretations, that is, interpre-
tations that satisfy all clauses

-+ x~x

x~y -+ y~x

x ~ y, y ~ z -+ x ~ z
x~y -+ f( ... ,x, ... )~f( ... ,y, ... )
x~y,P( ... ,x, ... ) -+ P( ... ,y, ... )

where f ranges over all function symbols and P over all predicate symbols.
The set of all these Horn clauses is denoted by EQ. We call I an equality
model of N if it is a model of N U EQ.
The fundamental inference rule in clausal theorem proving is resolution:

r -+ ~,A B,A -+ II
if u is a most general
ru, Au -+ ~u, IIu unifier of A and B.

The conclusion of a resolution inference is called a resolvent of the respective

premises. Resolution is refutationally complete for general clauses (without
 HORN CLAUSES WITH EQUALITY 93

equality) when combined with the factoring rules

r,A,B -+ L\ r -+ L\,A,B
and
ru, Au -+ L\u ru -+ L\u, Au
where u is a most general unifier of A and B.
Clauses with equality require additional inference rules, called paramod-
ulation:
r -+ L\,s ~ t A,A[u] -+ II r -+ L\,s ~ t A -+ II,A[u]
and
ru, Au, Au[tu] -+ L\u, IIu ru, Au -+ L\u, IIu, Au[tu]

where u is a most general unifier of s and u and u is not a variable. We

also speak of a paramodulation of the clause r -+ L\, s ~ t on the clause
A, A[u] -+ II (or A -+ II, A[u]).
Various restricted versions of resolution and paramodulation (without
factoring) can be shown to be refutationally complete for Horn clauses with
equality. We shall present one such inference system that also includes
simplification and deletion rules.

Definition 4.25. By a (positive) unit resolution we mean a resolution in-

ference in which one of the two premises is a (positive) unit clause. A
positive unit resolution
-+ A B,r -+ B'
ru -+ B'u
is said to be ordered (with respect to ~) if the atom Bu is maximal in ru
(i.e., there is no atom B" in r such that B"u ~ Bu).

By PR~ (N) we denote the set of all ordered positive unit resolvents obtain-
able from clauses in N. Positive unit resolution is a refutationally complete
inference rule for Horn clauses without equality (Henschen and Wos 1974).

Definition 4.26. Paramodulation inferences

-+ s ~ t A[u], r -+ B -+ s ~ t -+ B[u]
or
Au[tu], ru -+ Bu -+ Bu[tu]

are called positive unit paramodulations. Such a paramodulation inference

is said to be ordered (with respect to H if (i) Au is maximal in ru, and
(ii) there exists a (ground) substitution r, such that (su)r ~ (tu)r and,
whenever A[u] or B[u] is an equality atom v[u] ~ w, then (vu)r ~ (wu)r.

By PP~ (N, N') we denote the set of clauses obtained by ordered paramod-
ulation of a positive unit clause in N on a clause in N'.
94 ORDERED COMPLETION

In this section, by a complete reduction ordering we mean a well-founded

ordering >- on atoms and terms, such that (i) s >- t implies u[su]p >- u[tu]p
and P( ... , su, ... ) >- P( ... , too, .. .), for all terms s, t, and u, positions p in
u, substitutions 00, and predicate symbols P; and (ii) the ordering is total
on ground terms (the Herbrand universe) and ground atoms (the Herbrand
base).
The inference system 1£>- (or simply 1£ if >- is clear from the context)
consists of the inference rules below, which apply to pairs N; E where N
is a set of Horn clauses and E a set of equations. If E is a set of equations,
we also denote by C(E) the set of all positive unit clauses --+ s ~ t, such
that s ~ tEE.
(1) Inference rules applied to equations:
N;E
DEDUCTION: if s ~E t
N;EU{s ~n t}

N;EU{s ~n t}
DELETION: if there is a proof P of
N;E s ~ t in E such that
..
s ~;SI:j t t >-0 P

(2) Inference rules to convert positive unit clauses to equations:

NU{--+s~t};E
CONVERSION:
N;EU{s~t}

(3) Inference rules applied to Horn clauses:

N;E
RESOLUTION: if C is a resolvent of
NU{C};E clauses in NU{--+ x ~ x}

N;E
PARAMODULATION: if C is a paramodulant
NU{C};E of a clause in C(E) on a
clause in N

SUBSUMPTION:
NU{C,D};E if C I b
N U {C}; E D proper y su sumes

NU{C};E
DELETION: if C is redundant in N U
N;E C(E)
 HORN CLAUSES WITH EQUALITY 95

=
A clause C f -+ d is said to subsume a clause D if D is of the form
fD', A -+ dD', II. If, in addition, D does not subsume C, we say that C
properly subsumes D.
The concept of redundancy of clauses is adapted from (Bachmair and
Ganzinger 1990a). Let >-. be an ordering on Horn clauses defined by:
(f -+ A) >-. (d -+ B) if either f >-mul d or else f =
d and A >- B.
Definition 4.27. A clause C is said to be redundant in a set of clauses N
(with respect to the reduction ordering >-) if for every ground instance C u
of C, there exist ground instances Ct, ... ,Cn of clauses in N, such that (i)
Ct, ... , C n 1= Cu and (ii) CD' >-. Ci, for all i.
Tautologies, for instance, are trivially redundant. More complicated sim-
plification techniques can be described by inference rules derived from dele-
tion, resolution, and paramodulation. For further details we refer to Bach-
mair and Ganzinger (1990b).
For example, the inference rule
N U {C[su]};E U {s ~ t}
SIMPLIFICATION:
N U {C[tD']};E U {s ~ t}
if C[su] >- C[tu]

is obtained by combining paramodulation and deletion.

Inference system 1£~ are sound in the following sense.
Lemma 4.28. If N; E 1-1( N' ;E', then every Herbrand model of N U
C(E) U EQ is also a model of N' U C(E') U EQ.
Proof. Resolvents and paramodulants are logical consequences of their
respective premises. Also, if s ~ t is true in an equality interpretation I,
then u[su]p ~ u[tD']p is true in I. Q.E.D.
Definition 4.29. A derivation in 1£~ is said to be fair if
(i) the set of ordered critical pairs CP~(Eoo) is a subset of the set of
all derived equations Ui Ei;
(ii) the set of ordered positive unit resolvents PR~ (N00 U {-+ :z; ~ :z;} )
is a subset of the set of all derived Horn clauses Ui Ni;
(iii) the set of ordered paramodulants PP~(C(Eoo), N oo ) is a subset of
the set of all derived Horn clauses Ui Ni; and
(iv) Noo contains no positive unit clause of the form -+ s ~ t.
Fair derivations by ordered completion component of 1£ result in ground
convergent sets of equations.
Lemma 4.30. Let >- be a complete reduction ordering. If Noo U Eoo is the
limit of a fair derivation in 1£~, then Eoo is ground convergent with respect
to >-.
96 ORDERED COMPLETION

In addition, we will prove that 1£ is refutationally complete for Horn clauses

with equality, for which purpose we need the following (well-known) lemma.

Lemma 4.31. (Lifting Lemma) Let Cu and Du be ground instances of

clauses C and D, respectively.
(1) Every (ordered positive unit) resolvent of Cu and Du is a ground
instance of some (ordered positive unit) resolvent of C and D.
(2) Let C be a clause - s ~ t and D be a clause A, A[u] - II, such that
u is not a variable (and C and D have no variables in common). Suppose
su = uu and C' is a (ordered) paramodulant fu, Au[tu] - !:iu of Cu on
Du. Then C' is a ground instance of a (ordered) paramodulant ofC on D.

A proof of the lemma can be found in Peterson (1983).

Theorem 4.32. (Refutation completeness) Let ~ be a complete reduction
ordering and N be a set of Horn clauses. If Nco U Eco is the limit of a fair
derivation in 1£>- from N, then N U EQ is unsatisfiable if Nco contains the
empty clause.

Proof. By soundness, every model of N is also a model of Nco. Thus, if

Nco contains the empty clause, then N U EQ has no model.
Suppose, on the other hand, that Nco does not contain the empty clause.
Let I be the Herbrand interpretation for which P(t!, ... ,tn ) E I if and only
if there exists a ground instance - P(s!, ... , sn) of some unit clause in
Nco U {- x ~ x}, such that ti -~>- Si, for all i. (By this definition, a
ground equality atom s ~ t is in I if a,;d only if there exists a ground rewrite
proof of s ~ tin Et,.) We claim that I is a model of EQUU(Ni UC(Ei)).
It can easily be seen from the definition that I is an equality interpre-
tation, and therefore is a model of EQ. Furthermore, any ground instance
of an equation in Eco is contained in I, which implies that I is a model
of every set of unit clauses C(Ei)' In addition, all unit clauses of Nco are
satisfied by I. It remains to be proved that I is a model of every set of
Horn clauses Ni.
Suppose some ground instance of a clause in Ui Ni is not satisfied by
I. Let C be a minimal such ground instance with respect to the ordering
~'. Furthermore, let C' be a clause in Ui Ni and u be a substitution,
such that C = C'u. We may assume, without loss of generality, that C'
is not properly subsumed by any other clause in Ui Ni' Also note that xu
is irreducible by Et" for all variables x, as otherwise C would not be a
minimal clause false in I. In other words, the substitution u is irreducible.
This will allow us to apply the Lifting Lemma in all cases below.
Now suppose C' is not a clause in Nco. Since C' is not properly sub-
sumed by any other clause, this means that C' was either converted to an
 HORN CLAUSES WITH EQUALITY 97

equation or was deleted at some point in the derivation. If C' was con-
verted to an equation, then C cannot be false in I. On the other hand,
if C' was deleted at some point, then there exist clauses Ct, ... , Cn , such
that CI,"" Cn 1= C and C >-' Ci, for all i. Since C is false in I, some
ground clause Ci also has to be false in I, contradicting the minimality of
C. Thus C' has to be a clause in N 00'
Consequently, C is some (non-unit) clause At, ... , Ak -+ A, where k ~
1, A ¢ I, and {At, ... , Ak} ~ I. Let us assume, without loss of generality,
that Al t A2 t ... t Ak.
If Al is an equality atom of the form t ~ t, then there is an inference
-+t~t t~t,A2, ... ,Ak -+A
A 2, ... ,Ak -+ A
by ordered resolution. By the fairness assumption and the Lifting Lemma,
the conclusion D of this inference is a ground instance of some clause in
Ui N i · But D is false in I and C >-' D, which contradicts our assumption
that C is a minimal false clause.
Suppose Al is an equality atom of the form S ~ t, where S >- t. Since
S ~ t is true in I, there exists a ground rewrite proof of S ~ tin Et,. The
term s is thus reducible by Et,; and hence there is an inference
-+ U ~ v s[u]p ~ t,A 2, ... ,Ak -+ A
s[v]p ~ t,A 2, ... ,Ak -+ A
by ordered paramodulation. Using the Lifting Lemma and the fairness
assumption, we may again infer that the conclusion D of this inference is
a ground instance of some clause in Ui Ni, which contradicts that C is a
minimal false clause.
Finally, let us suppose Al is a non-equality atom P(tl' ... , tn). Then
there is some unit clause -+ P(Sb"" sn) in N oo , such that ti -+Eoo Si, for
all i with 1 :5 i :5 n.
If Si = ti, for all i, then there is an ordered resolution inference
-+ P(ti,"" tn) P(tt, ... , tn), A 2, ... , Ak -+ A
A 2, ... ,Ak -+ A
On the other hand, if ti -+ ~oo Si, for some i, then ti is reducible by Et" so
that there is an ordered paramodulation inference
-+ u ~ V P(t l , ... , ti[u]p, ... ,tn ),A2 , ... ,Ak -+ A
P(tl,' .. ,ti[V]p,' .. ,tn ), A 2, ... ,Ak -+ A
In either case we may use the Lifting Lemma and fairness to infer that the
conclusion D of the inference is a clause in Ui Ni, which contradicts that
C is a minimal false clause.
98 ORDERED COMPLETION

We conclude that no ground instance of a clause in U, N, is false in I.

In particular, I is a model of N = No. Q.E.D.

Dershowitz (1990) has used proof orderings to establish a proof normal-

ization result of an inference system for conditional equations that corre-
sponds to a specific version of the system 1£ above. (The deduction rules
are essentially the same as in 1£, but the simplification rules are weaker and
can be derived from deletion, resolution, and paramodulation.)
Paul (1986) has studied the application of standard completion to Horn
clauses with equality. The word problem in Horn clause theories has been
studied by Kounalis and Rusinowitch (1987).

Summary
We have presented an extension of standard completion, called ordered
completion, which is designed to construct a set of equations that is ground
convergent with respect to a complete reduction ordering. A fair ordered
completion procedure is guaranteed to succeed in constructing a ground
convergent system. Furthermore, we have proved that a specific version of
ordered completion, called unfailing completion (which also extends stan-
dard completion), always succeeds in constructing a convergent (and not
only a ground convergent) rewrite system, provided the given reduction
ordering is completable.
Ordered completion is also a refutationally complete theorem prover for
purely equational theories. We have discussed further applications of the
method to Horn clauses with equality, and have obtained a refutationally
complete inference system that combines ordered paramodulation (for the
equational part) with ordered positive unit resolution and ordered positive
unit paramodulation (for the Horn clause part) and also includes powerful
rules for deletion of redundant clauses.
The techniques underlying ordered completion have also been applied to
A-unification and "rigid unification," a form of unification of importance
in theorem provers based on equational matings; see Gallier and Snyder
(1989), Gallier, Snyder, and Raatz (1989) and Gallier, et al. (1988). For
another interesting application, to unification in Boolean rings and Abelian
groups, see Boudet, Jouannaud, and Schmidt-SchauB (1988). Reddy (1989)
found the approach to be of advantage in describing rewrite techniques for
program synthesis. Applications to first-order theorem proving (with or
without equality) are described in Bachmair and Dershowitz (1987).
5. PROOF BY CONSISTENCY

In many applications, such as algebraic data type specifications and equa-

tional programming, equations are intended to define a certain standard
model, called the "initial model." Reasoning about algebraic data types
and equational programs thus requires proof methods for this initial algebra
semantics. Such proof methods typically employ some induction scheme,
e.g., induction on the structure of terms. We shall discuss an alternative
approach-proof by consistency-that can be applied to equational theories
that are presented as ground convergent rewrite systems.

5.1. Consistency and Ground Reducibility

Definition 5.1. An equation s ~ t is said to be an inductive theorem of a
set of equations E, written s =I(£) t, if su ...... :;.; tu, for all ground equations
su ~ tu.

For example, associativity and commutativity, (x + y) + z ~ x + (y + z)

and x + y ~ y + x, are inductive theorems of Ro = {x + 0 - x, x + S(y) -
S(x + y)}. (They are not theorems, though, as there are models of Ro in
which the function denoted by + is not associative and commutative.)
Dershowitz (1982a) has pointed out that an equation s ~ t is an induc-
tive theorem of a (ground) convergent rewrite system R if and only if no
equation 1.1 ~ v, where 1.1 and v are distinct ground terms irreducible by R,
is provable in R U {s ~ t}. Thus, if s ~ t is an inductive theorem of R, then
any (ground) convergent rewrite system for R U {s ~ t} defines the same
ground normal forms as R.l
Let R be a terminating rewrite system that is ground convergent with
respect to the reduction ordering -1i. (That is, for all ground terms sand
t with s ...... 'R t, there exists a ground term v, such that s -'R v +-'R t.) We
also write s -R! t if s -'R t and t is in normal form.
Definition 5.2. We say that an equation s ~ t is consistent with R if, for
every ground equation su ~ tu, the two terms su and tu can be reduced
1 H R is ground convergent, then the algebra defined on the set of ground normal-form
terms is an initial model of R (Goguen 1980).

99
100 PROOF BY CONSISTENCY

8eT ...- - - - - - . teT

c

R! R!

8' t'

Figure 5.1: Inconsistency

to identical normal forms by R. Otherwise, s ~ t is said to be inconsistent

with R.

A set of equations C is said to be consistent with R if all its equations are

consistent with R; and inconsistent, otherwise (see Figure 5.1). Roughly
speaking, consistency expresses in proof-theoretical terms that the two sets
of equations Rand R U {s ~ t} define the same initial algebra.

Proposition 5.3. (Dershowitz 1982a) A set of equations C is consistent

with a ground convergent rewrite system R if and only if all equations in C
are inductive theorems of R.

Proof. Let s ~ t be any equation in C. If C is consistent with R, then

SeT f-+R to", for all ground equations so" ~ to". Consequently, s ~ t is an
inductive theorem of R.
On the other hand, suppose that all equations in C are inductive the-
orems of R. If so" ~ to" is a ground instance of an equation in C, then
so" f-+R to" and, since R is ground convergent, the two terms so" and to"
can be reduced to a common normal form by R, which implies that C is
consistent with R. Q.E.D.

Consistency-in the above sense-is not decidable. However, we will

show that any (finite) inconsistent set of equations C can be transformed
into a "provably inconsistent" set. The key here is the notion of "ground
reducibility."

Definition 5.4. (Jouannaud and Kounalis 1986). A term t is ground re-

ducible by R if all its ground instances are reducible by R.

For example, if Ro = {x + 0 ---. x, x + S(y) ---. S( x + y)}, then any term

in which the function symbol + appears is ground reducible by Ro.
 PROOF BY CONSISTENCY 101

Ground reducibility is decidable for finite rewrite systems (Plaisted

1985; Kapur, Narendran, and Zhang 1987), but is provably in exponen-
tial time, even for left-linear rewrite system (Kapur, et. al. 1987). Al-
gorithms for deciding ground-reducibility with respect to left-linear rewrite
systems have been described by Jouannaud and Kounalis (1986) and Kapur,
Narendran, and Zhang (1986). In theories with free constructors ground
reducibility is trivially decidable: a term is ground reducible if and only if
it contains a non-constructor symbol (cf. the discussion of constructors in
Huet and Hullot 1982; Jouannaud and Kounalis 1986; and Fribourg 1989).
What we actually need, however, is a suitable notion of ground reducibil-
ity for equations.
Definition 5.5. We say that an equation s ~ t is ground reducible by R
if, for every ground equation su ~ tu, the two terms su and tu are identical
whenever they are both irreducible by R.2
In other words, an equation s ~ t is not ground reducible if there exists a
ground equation su ~ tu for which su and tu are irreducible, yet distinct.
For example, the equation x + y ~ y + x is ground reducible by Ro, but
S(S(x)) ~ S(x) is not, as there is a ground instance, S(S(O)) ~ S(O), in
which both terms are irreducible, yet distinct.
Decision procedures for testing ground reducibility of terms can easily
be adapted to the problem of checking ground reducibility of equations.
LeIllIlla 5.6. If C is consistent with R, then all equations in C are ground
reducible.
Proof. Suppose some equation s ~ t in C is not ground reducible by R.
Then there has to be some ground instance su ~ tu wherein both su and
tu are irreducible, yet distinct. Hence C is not consistent with R. Q.E.D.
The reverse direction is not true: a set of ground reducible equations
need not be consistent. For instance, the equation S(S(x + 0)) ~ S(x + 0)
is ground reducible by Ro, but not consistent with Ro.

5.2. Proof by Consistency

We say that two reduction orderings >-1 and >-2 are compatible if the tran-
sitive closure of their union is also a reduction ordering. (In other words,
compatibility means that the transitive closure of >-1 U >-2 is well-founded.)
Let R be a finite ground convergent rewrite system and >- be a reduction
ordering compatible with the reduction ordering -1l.
2This notion of ground reducibility of equations is different from the notion of "co-
reducibility" introduced by Jouannaud and Kounalis (1986).
102 PROOF BY CONSISTENCY

Definition 5.7. A set of equations e is said to be provably inconsistent

with R (relative to >-) if it contains either an equation that is not ground
reducible by R, or an equation s ~ t, where s >- t and s is not ground
reducible by R.
In other words, if e is provably inconsistent with R, then there exists a
proof
sI = A
SfT +-+.l':It
t fT = t '
or
S
I
= SfT +-+.l':It
A t fT -+R! t '
in RUe, where s' and t' are irreducible by R and s' :I t'. (The inconsistency
test used by Jouannaud and Kounalis (1986) in their inductive completion
procedure is based on the existence of proofs of the latter form.)
Lemma 5.S. Every provably inconsistent set of equations is inconsistent.

Proof. Suppose e is provably inconsistent with R. By Lemma 5.6, if some

equation in e is not ground reducible by R, then e is inconsistent with R.
On the other hand, if e contains an equation s ~ t, such that s >- t and s
is not ground reducible, then there exists a ground proof SfT +-+c tfT -+R! t/,
wherein SfT and t' are irreducible. Since SfT >- tfT >- t/, the two normal forms
SfT and t' are distinct, which implies that e is inconsistent. Q.E.D.
It is decidable whether a given (finite) set of equations e is provably
inconsistent (provided the ordering >- is decidable). On the other hand, if
e is inconsistent, but not provably inconsistent, then there exists a ground
proof P of the form

where S ~ t is an equation in e, such that t 'f S and s' and t' are distinct
irreducible terms. We can deduce new equations from R and e to repeat-
edly simplify this proof until eventually a provably inconsistent set e' is
obtained.
First note that we may assume without loss of generality that the sub-
stitution fT is irreducible, in the sense that ZfT is irreducible, for all variables
z. For suppose ZfT were reducible by R, for some variable z. Let p be the
substitution for which zp is the normal form of ZfT, and let pi be the proof

We have SfT -+~ S' or s' = SfT. If S' = SfT, then s 'f t and tp -+~ t/, as
otherwise e would be provably inconsistent. In either case, pi is a proof of
the desired form.
 PROOF BY CONSISTENCY 103

Figure 5.2: Proof simplification

Let us therefore assume that P is a proof as above, where in addition

(1' is an irreducible substitution. Then the subproof

is a proper overlap. (We assume, without loss of generality, that u R:: v and
s R:: t have no variables in common.) By the Critical Pair Lemma, there
exist a critical overlap ST[VT]p +-~s::su ST +-+~s::s, tT and a substitution (1",
such that (ZT)(1" = Z(1', for all variables Z in S R:: t or u R:: v. Furthermore,
the proof

is simpler (according to some well-founded complexity measure on proofs

to be defined below) than the proof P (cf. Figure 5.2). This proof sim-
plification process constitutes the basis of our proposed inductive theorem
proving method.

Let R be a ground convergent rewrite system and >- be a reduction

ordering compatible with -+~. By CP(R, C) we denote the set of all critical
pairs of an equation in R on an equation in C. The inference system P1i
(or simply P if Rand >- are clear from the context) consists of the following
inference rules, where C may be any set of equations ("conjectures") and
104 PROOF BY CONSISTENCY

L any set of inductive consequences ("lemmas") of R:

L;C
DEDUCTION: if s ~ t E CP(R,CU C- 1 )
L;CU{s~t}

L;CU{s~t}
DELETION: if S =Z(R) t
L;C

L;C
INDUCTION: if S =Z(R) t
LU{s~t};C

L;CU{s~t}
SIMPLIFICATION: if s >- u and either s .......~UL
L;EU{u~t}
u or else s .......~~w u, for
some equation v ~ w in C,
such that s t> v and v >- w

where the symbol t> denotes the strict part of the encompassment ordering.
(As usual, we assume that the label of an equation indicates to which of
the sets R, L, or C it belongs.)
The deduction rule suffices to derive a provably inconsistent set from any
inconsistent set of conjectures. The remaining inference rules are essential,
however, for possibly verifying that a given set of conjectures is consistent.
Once a conjecture has been established as an inductive theorem, it can
be deleted and then added as a lemma, by the corresponding inference
rules. The induction rule can be applied to any inductive theorem s ~ t
(even if that theorem was proved by some other proof method). In this
sense, proof by consistency can be combined with other inductive theorem
proving methods. The inductive theorems in L can be used to simplify
a conjecture, but no new equations need to be deduced from them. The
introduction of additional lemmas therefore does not increase the search
space of proof by consistency.
Each equation can be simplified before any consequences are deduced
from it. Simplification by equations in C is slightly more restrictive than
necessary. For instance, a conjecture s ~ t in C cannot be simplified by any
other conjecture s ~ u. (The inference rule can easily be generalized by
taking the labels into account, in a similar way as for ordered completion.)
Simplification by equations in R U L is unrestricted, and only the final
term u, but none of the intermediate terms in the proof s ....... ~UL u is re-
quired to be smaller than s. For instance, if commutativity and associativity
are known to be inductive theorems, then equations can be simplified by
associative-commutative rewriting. (But in contrast with the associative-
commutative inductive completion procedure suggested by Jouannaud and
 PROOF BY CONSISTENCY 105

Kounalis (1986), proof by consistency does not use associative-commutative

unification when deducing new equations.)
Inference systems P are sound in the following sense.

Proposition 5.9. (Soundness) Let R be a ground convergent system. If

L ; C I-'PR L' ; C', then C is consistent with R if and only if C' is.

For example, from the rewrite system Ro = {x + 0 -+ x, x + S (y) -+

S(x + y)} and the conjecture x + y ~ y + x, we can derive new equations
0+ x ~ x and S(x) + y ~ S(x + y). The set of all derived equations can
be shown to be consistent (as we shall describe below). By soundness, all
equations are inductive theorems of R.

Definition 5.10. By a proof by consistency procedure we mean any pro-

gram that accepts as input a ground convergent system R, a reduction
ordering >- compatible with -+"k,
a set L of inductive theorems of R, and
a set of conjectures C; and uses the inference rules of P'Ji. to generate a
derivation from L U C.

A characteristic of proof by consistency procedures is that they are lin-

ear, in that all new equations are deduced by superposing rules from the
initial rewrite system R on (initial or deduced) conjectures. The proce-
dure by Fribourg (1989) is a proof by consistency procedure in this sense,
while most so-called inductive completion procedures are not. The latter
procedures are essentially standard completion procedures augmented by a
consistency check and compute all critical pairs in CP(R U C), e.g., also
critical pairs between conjectures.3
Musser (1980) was the first to describe an inductive completion proce-
dure. His procedure applies to abstract data type specifications, where an
equality predicate eqD is associated with each data type D and the speci-
fication is "sufficiently complete," so that each ground expression eqD(s, t)
can be reduced to the Boolean constant true or false. The equation
true ~ false indicates an inconsistency. Various improvements of the basic
scheme have been described by Huet and Hullot (1982), Lankford (1981),
Dershowitz (1982a), Jouannaud and Kounalis (1986), Fribourg (1989), and
Kapur, Narendran, and Zhang (1986). The various approaches mainly dif-
fer in the respective notions of consistency they employ.
Huet and Hullot (1982) studied the case oftheories with (free) construc-
tors, in which case an inconsistency is signified by an equation between two
3Given a ground convergent rewrite system R, an equation s ~ t is an inductive
theorem of R if the completion procedure constructs a convergent system for R u {s ~ t}
without deriving an inconsistency, while the equation is not an inductive theorem if
completion does derive an inconsistency.
106 PROOF BY CONSISTENCY

distinct ground terms built solely from constructor symbols. In contrast

with Musser's method, an explicit axiomatization of equality is not required
in this context.
Jouannaud and Kounalis (1986) design an inductive completion proce-
dure based on ground reducibility of terms. An inconsistency is signified
by a rewrite rule u - v the left-hand side of which is not ground reducible.
In a similar procedure by Kapur, Narendran, and Zhang (1986) "test sets"
are used to check for consistency.
The method proposed by Fribourg (1989) can be viewed as a linear
restriction of inductive completion or as a proof by consistency procedure.
The use of a linear deduction strategy may considerably restrict the number
of equations to be deduced, so that the search space is smaller. In fact, many
of the equations that have to be deduced in order to construct a (ground)
convergent rewrite system may be irrelevant for proving a given inductive
theorem. In essence, full inductive completion corresponds to attempting to
solve all possible induction schemes-and fails to terminate if one induction
schema diverges. Linear proof by consistency procedures, on the other
hand, may select one specific induction schema. As a consequence, a proof
by consistency procedure may succeed in proving inductive theorems for
which inductive completion does not terminate; see Fribourg (1989) for an
example. On the other hand, it is also possible that full completion may
deduce useful lemmas that cannot be obtained by the more restrictive linear
deduction mechanism of a proof by consistency procedure.
Example 5.11. (Kiichlin 1989) Let R be the ground convergent rewrite
system
app(ni/, z) - z
app(cons(z, y), z) - cons(z, app(y, z»
rev (nil) - nil
rev(cons(z,y» - app(rev(y),cons(z,ni/»
and suppose rev(rev(z» :::::: z is to be established as an inductive theorem
of R.
The last rule in R can be superposed on the given conjecture, resulting
in a critical pair
rev(app(rev(y), cons(z, nil))) :::::: cons(z, y).
If we superpose the initial conjecture rev( rev( z» : : : zon this new con-
jecture, we obtain a critical pair
rev( app(y, cons( z, nil))) :::::: cons( z, rev(y»
which can be oriented into a rule
rev(app(y, cons(z, nil))) - cons(z, rev(y»
 REFUTATION COMPLETENESS 107

(with respect to a suitable lexicographic path ordering). The first critical

pair can now be simplified and deleted. The remaining set of rewrite rules
is ground convergent, which implies that rev( rev( ~ z» z
is an inductive
theorem of R.
On the other hand, with a linear deduction strategy the above rewrite
rule cannot be deduced and an infinite derivation
rev(app(rev(y) , cons(z, nil))) ~ cons(z, y)
rev(app(app(rev(z), cons(y, nil», cons(z, nil» ~ cons(z, cons(y, z»

may be produced.
In general, the inference rules of P do not change the initial ground
convergent system R, whereas with inductive completion the goal is the
construction of a (ground) convergent rewrite system for R U C and the
initial system R need not be retained.
One of the main problems with full inductive completion is that, like
standard completion, it must be supplied with an ordering on terms which
is used to orient equations into rewrite rules and may fail if an equation
is generated that cannot be oriented in the given ordering. An important
advantage of proof by consistency is that unorientable equations can be
handled and any ordering on terms that is compatible with the rewrite
relation --+k may be used. Proof by consistency does not fail and in fact is
a complete method for disproving inductive theorems. 4

5.3. Refutation Completeness

A proof by consistency procedure is said to be refutationally complete if
from every inconsistent set of conjectures Co it generates a derivation for
which some set Ci is provably inconsistent.
The derivation of a provably inconsistent set of equations can be viewed
as a proof normalization process. In this context, we are interested in proof
transformations that apply to proofs of the form
s' +-R su +-+c tu --+R t'
where s' and t' are distinct terms irreducible by R. A normal-form proof is
a proof UT +-+c VT, wherein UT is irreducible and either VT is also irreducible
and distinct from UT, or else U >- v. The existence of such a normal-form
proof implies that the set C is provably inconsistent.
fThe inference system l' thus solves problem P146 posed by J.-P. Jouannaud in
Bulletin of tlJe EATCS 31, February 1987.
108 PROOF BY CONSISTENCY

We first introduce a suitable complexity measure on proofs. The cost

of a single proof step su +-+~::=t tu is defined to be:

({su},s,tu) if s >- t
{ ({tu}, t, su) ift>-s
({su,tu},.1,.1) otherwise

(The cost assigned to other proof steps, which are not of this form, is
irrelevant. )
If P is a ground proof of the form U -R su +-+~::=t tu -R v, where u
and v are not equivalent in R, then the complexity -yP of P is the cost of
the proof step su +-+~::=t tu. If P is the empty proof, then -yP = (T,.1, .1).
In all other cases, -yP = (T, T, T).
If >- is a reduction ordering compatible with -~, we denote by >-R the
transitive closure of the union of>- and -~; and by I>R the transitive
closure of the union of >- R with the proper subterm ordering. The ordering
I>R is well-founded, but not necessarily a rewrite relation. 5 It contains
both the rewrite relation - ~ and the reduction ordering >-.
Proofs are compared according to their complexity, using the lexico-
graphic combination of the multiset extension of the ordering I> R (in the
first component), the encompassment ordering I> (in the second compo-
nent), and the ordering I>R (in the last component). As usual, T and .1
are assumed to be maximum and minimum elements with respect to each
ordering. We denote this lexicographic ordering by >-P and write P tp Q
if -yP !:P -yQ. In other words, we have P >-p Q if -yP >-P -yQ. The strict
ordering >-p is well-founded.
The inference rules of P never increase the complexity of proofs.

Lemma 5.12. Suppose £ ; C I-p £' ; C' and let P be a proof of an equation
s' ~ t' in R U C. Then there is a proof P' in R U C', such that P tp P',
if s' ~ t' is an inductive theorem of R, and P !:p P', if s' ~ t' is not an
inductive theorem.

Proof. Suppose £; C I-p £' ; C' and let P be a proof in R U C. If P is a

proof of an inductive theorem of R, then -yP !:P (T,.1,.1). Let P' be the
empty proof. Clearly, we have P tp P'.
On the other hand, suppose P is a ground proof s' -R su +-+;::=t tU-R
t', where s ~ t is an equation in C and s' and t' are not equivalent in R.
Since rewrite steps in R do not contribute to the complexity of a proof, we
may assume, without loss of generality, that s' and t' are irreducible by R.
5The subterm ordering is not a rewrite relation. For eXaIIlple, x is a subtenn of x-,
but x + y is not a subtenn of x- + y.
 REFUTATION COMPLETENESS 109

If P is a proof in RUG', let P' be P. If P is not a proof in RUG', then

G' is (G \ {8 ~ t}) U {u ~ t}, where 8 >- u and either 8 -1iUL u, or else
8 -~R:lW u where v ~ W is an equation in G, such that 8 I> v and v >- w.
(The equation 8 ~ t cannot be deleted, as it is not an inductive theorem.)
Let u' be the normal form of UtT.
( a) If u' ~ t', let P' be the proof u' - R UtT -!R:lf ttT -+ Rt'. Then the
complexity of P' is the cost of the proof step UtT -!R:lf ttT. We show that
P >-p P'.
(i) If 8 >- t, then r P = ({ 8tT}, 8, ttT). The first component of r P ' is
{UtT, ttT}, {UtT}, or {ttT}, all of which are smaller than {8tT} (with respect to
the multiset extension of I> R), so that P >-p P'.
(ii) 1ft >- 8, then r P= =
({ttT},t,8tT) >-p ({ttT},t,UtT) r P '.
(iii) If neither 8 >- t nor t >- 8, then r P = ({ 8tT, ttT}, 1., 1.), while the
first component of r P ' is {UtT, ttT} or {ttT}, both of which are smaller than
{8tT, ttT}.
(b) If u' = t', then u' :f:. 8'. Since 8 -1iUL u implies that 8' and u' are
identical, this case only arises if 8 -~R:lW U for some equation v ~ winG,
such that 8 I> v and v >- w. Let T be a substitution, such that 81p = VT
and ulp = WT, and let v' and w' be the (ground) normal forms of VTtT and
WTtT, respectively. Note that 8' :f:. u' implies v' :f:. w'.
Let P' be the proof v' -R VTtT -~R:lW WTtT -+R w'. Since v >- w, the
complexity of P' is ({VTtT} , v, WTtT). The complexity of Pis ({8tT},8,ttT), if
8>- tj ({ttT}, t, tT), if t >- 8j and ({8tT, ttT}, 1., 1.), otherwise. Considering the
different cases and using the fact that VTtT is a subterm of 8tT and 8 I> v,
we conclude that P >-p P'. Q.E.D.

Derivations for which proof normalization yields the desired result can
be characterized by an appropriate fairness condition.

Definition 5.13. We say that G' is a covering set for G (or G' covers G)
with respect to Rand >- if, for every ground proof P = 8tT -:R:lf ttT in G,
such that (i) the substitution tT is irreducible by R, (ii) 8tT is reducible by
R, and (iii) t 'f 8, there exists a ground proof Q in G', such that P >-p Q.
Observe that if 8tT and ttT are equivalent in R, then P >-p Q, for the empty
proof Q. Consequently, the empty set is a covering set for any consistent
set G. It is also evident from the definition that if G' covers G, then any
superset of G' covers any subset of G. Moreover, if G~ covers G1 and G~
covers G2 , then q U G~ covers G1 U G2 •

Definition 5.14. A derivation Lo j Go rp L1 j G1 rp L2 j G2 rp ... is said

to be fair if the set Ui Gi of all deduced equations covers the set Goo of all
persisting conjectures.
110 PROOF BY CONSISTENCY

A proof by consistency procedure is fair if it produces only fair derivations.

With these definitions, we have:
Theorem 5.15. If Lo ; Co I-p Ll ; C l I-p L 2 ; C2 I-p ... is a fair deriva-
tion, where Co is inconsistent with R, then some set Ci is provably incon-
sistent.
Proof. Let Lo ; Co I-p Ll ; C l I-p L2 ; C2 I-p ... be a fair derivation, where
Co is inconsistent with R. We show that some set Ci is provably inconsis-
tent. If Co is provably inconsistent, we are done. Let us assume Co is not
provably inconsistent.
We first prove that whenever P is a proof s' -1i su +-+:=t tu -R t'
in R U Ci, such that s' and t' are distinct, irreducible ground terms, the
substitution u is irreducible, and t 'I s, then there is a proof P' in R U Cj,
for some j ~ 0, such that P >-p P'. By Lemma 5.12, this is true whenever
s ~ t ¢ Coo. Suppose the equation s ~ t is in Coo. By fairness Uk Ck
covers {s ~ t}. Thus there exists a ground instance UT ~ VT of an equation
U ~ v in Cj, for some j ~ 0, such that su +-+:=t tu >-p UT +-+!=v VT. Then
P >-p P', where P' is the proofu' -R UT +-+c; VT -R v' and u' and v' are
normal forms of UT and VT, respectively.
Let now Pi o be a proof s' -1i su +-+Co tu - R t', where s' and t' are
distinct terms irreducible by R and u is an irreducible substitution. (Since
Co is not provably inconsistent, there exists such a proof.) Then there is
a sequence of proofs P io ' P il , P i3 , ... where Pi; is a proof in R U Ci; and
Pi;_l >-p Pi;, for all j > 0. Since >-p is well-founded this sequence must
be finite. In other words, some proof Pi" is of the form su +-+C" tu -R t',
where su is irreducible and either s >- t or else tu is irreducible and distinct
from su. But then Ci " is provably inconsistent. Q.E.D.
Fair derivations always exist.
Lemma 5.16. The set of all critical pairs of rules in R on equations in
C U C- I is a covering set for C.
Proof. Let C' be the set of all critical pairs of rules in R on equations
in C U C-I and let P be a ground proof su +-+:=t tu in C, where the
substitution u is irreducible by R, su is reducible by R, and t 'I s. We have
to show that there exists a ground proof Q in C', such that P >-p Q. This
trivially holds if su and tu are equivalent in R. Let us assume this is not the
case. Since u is irreducible, but su is reducible by R, there exist a critical
pair U ~ v of some rule in R on the equation s ~ t and a substitution T,
such that su -RUT and tu = VT.
Let Q be the proof UT +-+~=v VT. The complexity of Q is ({ UT}, U, VT),
if s >- v; ({VT},V,UT), if v >- u; and ({UT,VT},.l,.l), otherwise. If s 'I t
 COVERING SETS 111

(in addition to t 'I- s), then the complexity of Pis ({sO',tO'},..L,..L). Since
sO' )-R UT and to' = VT, we conclude that in this case P )-p Q. On the other
hand, if s )- t, then the complexity of P is ( {sO'}, s, to'). Since sO' )- R UT and
sO' )-R to' = VT, we again have P )-p Q. In sum, the set CP(R, C U C- 1 )
indeed covers C. Q.E.D.

The lemma indicates that covering sets can be computed for all finite sets
of equations C. As a consequence, we obtain:

Proposition 5.17. Let Co be a finite set inconsistent with R. Then there

is a derivation Lo ; Co I-p L1 ; C1 I-p L2 ; C2 I-p ... wherein some set Ci IS
provably inconsistent.

In practice, fair derivation are constructed by employing some schema

of marking those equations for which covering sets have already been com-
puted. To guarantee fairness a covering set has to be computed for each
unmarked equation. If the initial set of conjectures Co is inconsistent, then
by the above theorem a provably inconsistent set will be produced even-
tually. If at any point in a derivation all equations are marked and no
provably inconsistent set was encountered, then all deduced equations in
Ui Ci are inductive consequences of R. Of course, a procedure need not nec-
essarily terminate for any consistent set, but may instead deduce ever more
inductive consequences without obtaining a verifiably consistent set. The
introduction of appropriate lemmas (e.g., by generalization as in Boyer and
Moore 1979) in conjunction with simplification may be of help in obtaining
a verifiably consistent set.

5.4. Covering Sets

Computation of covering sets is usually based on critical pairs, but it is not
always necessary to compute all critical pairs of R on C U C'. For instance,
if s ~ t is an equation with s)- t, then CP(R, {s ~ t}) is a covering set for
{s ~ t}. In other words, critical pairs which are obtained by superposing on
the smaller term t are superfluous. This restriction conforms to the usual
practice in completion procedures, but in proof by consistency procedures
even more critical pairs can usually be eliminated.

Definition 5.1S. (Fribourg 1989) A position p in a term t is said to be

inductively complete (with respect to R) if tip is not a variable and each
ground term tO'lp is an instance of some left-hand side of R, whenever 0' is
irreducible.
112 PROOF BY CONSISTENCY

In other words, if P is an inductively complete position in t, then each

ground instance to' is reducible either within the variable part of t or at
position p.
For example, take the rewrite system Ro = {x + 0 ..... x, x + S(y) .....
S(x + ynand let s be the term x + (y + z). The position P = (2), referring
to the subterm y + z, is inductively complete.
If P is an inductively complete position in a term s, then the set of all
critical pairs obtained by superposing rules in R on the equation s R:I t at
position P in s is a covering set for {s R:I t}. As Fribourg (1989) points out,
choosing an inductively complete position in a term, if one exists at all,
essentially corresponds to selecting an "induction schema."
For example, the associativity of addition, x + (y + z) R:I X + y) + z, is
an inductive consequence of the above set R. Let >- be the lexicographic
path ordering based on a precedence >-p in which + >-p S >-p o. We obtain
a covering set for {x + (y + z) R:I (x + y) + z} by superposing on the left-
hand side x + (y + z) at position P = (2). There are two critical pairs,
x + y R:I (x + y) + 0 and x + (y + S(z)) R:I (x + y) + S(z), the first of which
can be simplified to a trivial equation x+y R:I x+y, while the second can be
simplified to a ground reducible equation S(x + (y + z)) R:I S«x + y) + z),
which is covered by {x + (y + z) R:I (x + y) + z}. Since the set of all
deduced equations covers all persisting equations and no inconsistency has
been derived, all deduced equations are inductive theorems of R.
In general, {s R:I t} is a covering set for {u[s]p R:I u[t]p}, whenever pi
A. More precisely, whenever uu[su]p R:I uu[tu]p is an inconsistent ground
instance, so is sO' R:I to', and in addition uu[su]p +-+~[$ll'=u[tl uu[tu]p >-p
SO' +-+;l'=t to'.
In a similar vein, in theories with free constructors the set of equations
{S1 R:I t 1, ... ,Sn R:I t n } can be shown to be a covering set for any equation
I(S1, ... ,Sn) R:I l(t1, ... ,tn ), where 1 is a constructor symbol (cf. Huet
and Hullot 1982). For if 1 is a free constructor, then a ground instance
I(S1U, ... ,snu) R:I l(t1U, ... ,tnu) is inconsistent if and only if one of the
equations SiU R:I tiu is inconsistent. Moreover, in such theories any equation
I(S1, ... , sm) R:I g(tl, ... , t n ), where 1 and 9 are different constructors, is
inconsistent.
The notion of an inductively complete position can be generalized in an
obvious way to sets of positions. A set {Pl. ... ,Pn} of non-variable positions
in a term t is said to be inductively complete if every ground instance to' is
reducible by R at some position Pi, whenever 0' is irreducible (cf. Kiichlin
1989, Biindgen and Kiichlin 1989).
Critical pair computations can often be restricted to inductively com-
plete sets of positions even when an equation S R:I t is unorientable. If sand
 COVERING SETS 113

t are both ground reducible, then both CP(R, {s ~ t}) and CP(R, {t ~ s})
are covering sets for {s ~ t}. Thus, superposition may be restricted to ei-
ther side of such an unorientable equation. (Proof by consistency differs
from ordered completion in this respect.)

Example 5.19. Let Ro be the rewrite system

x+O -+ x x*O -+ 0
x + S(y) -+ S(x + y) x*S(y) -+ x*y+x

and >- be the recursive path ordering corresponding to a precedence >-p in

which * >-p + >-p S >-" O. Furthermore let Lo be the set of lemmas

x+y ~ y+x
x+(y+z) ~ (x+y)+z

We prove that the set of conjectures

x * (y + z) ~ x *y + x *z
x*y ~ y*x
x*(y*z) ~ (x*y)*z

is consistent with Ro.

First observe that x * (y + z) >- x * y + x * z. Hence we obtain a covering
set for the distributivity equation by superposing on position p = (2) of
its left-hand side. There are two critical pairs, x * y + x * 0 ~ x * y and
x *y+ x *S(z) ~ x* S(y+ z), the first of which can be simplified to a trivial
equation x*y ~ x*y and deleted. Since x*y+x*S(z) -+Ro/Lo (x*y+x*z)+x
and x * S(y + z) -+Ro X * (y + z) + x -+c (x * y + x * z) + x, the second
equation can also be simplified and deleted.
Superpositions on the commutativity axiom x*y ~ y*x can be restricted
to the left-hand side, as both x*y and y*x are ground reducible. This results
in two critical pairs, 0 * x ~ 0 and S(y) * x ~ x * y + x, both of which are
ground reducible and can be used as rewrite rules. Computation of covering
sets results in four new equations, three of which can be simplified to trivial
equations. The remaining equation, S(y) * x + S(y) ~ S(x) * y + S(x), can
be simplified by -+t/Lo to S(x * y + (x + y)) ~ S(y * x + (x + y)), an
equation which is already covered by the commutativity axiom.
Finally, to deal with the associativity axiom x * (y * z) ~ (x * y) * z, we
superpose all rules in Ro at the top-most position of the right-hand side of
the equation and obtain a covering set of two equations, x * y ~ x * (y * 0)
and (x * y) * z + (x * y) ~ x * (y * S( z)). The first equation can be simplified
to a trivial equation x * y ~ x * y; the second, to (x * y) * z + (x * y) ~
114 PROOF BY CONSISTENCY

z * (y * z) + (z * y). The latter equation is covered by the associativity

axIom.
In summary, all persisting equations are ground reducible and the set of
all deduced equations covers the set of all persisting equations. Hence, all
deduced equations, including the initial conjectures, are inductive theorems
of Ro.

Example 5.20. Let R1 be the rewrite system Ro extended by the rules

d(O) -+ 0
d(S(z» -+ S(S(d(z»

and let L1 be Lo plus all inductive theorems proved in the previous example.
Then
I
d( z) -+ z + z I
is an inductive theorem of R 1 •
Let us assume the lexicographic path ordering from the previous exam-
ple is extended so that in the underlying precedence d >-p *. Then d(z) >-
z + z and it suffices to superpose on d(z) to get a covering set for the given
conjecture. The critical pairs are 0 ~ 0 + 0 and S(S(d(z))) ~ S(z) + S(z),
both of which can be reduced to trivial equations. For example,

S(S(d(z))) -+R 1 S(S(z + z» +-RdLl S(z) + S(z).

Example 5.21. Let R2 be the rewrite system Ro extended by the rules
-+

and let L2 =
L 1 . Again, we assume the lexicographic path ordering is
extended by assigning highest precedence to the new function symbol. The
conjecture
I
z!l+z ~ z!l * ZZ I
is covered by two critical pairs z!l ~ z!l * ZO and zS(!I+ z) ~ z!l * zS(z). We
have

and
ZS(!I+ Z ) -+R, z * z!l+z -+c z * (z!l * ZZ) +-R,/L, z!l * zS(z)
which indicates that both critical pairs can be reduced to trivial equations.
Since all persisting equations are covered, this establishes that z!l+z ~
z!l * ZZ is an inductive theorem of R2.
 COVERING SETS 115

Example 5.22. Let R3 be the rewrite system Ro extended by the rules

sum(O) - 0
sum(8(z» - sum(z) + 8(z)
and let L3 = L 1 • The conjecture

I sum(z) + sum(z) R:l z * 8(z) I

is covered by two critical pairs, sum(O)+O R:l 0*8(0) and (sum(z)+8(z»+
sum(8(z» R:l 8(z)*8(8(z». Both critical pairs can be simplified to trivial
equations. For example, we have

(sum(z) + 8(z» + sum(8(z»

-R3 /L s (8(z) + 8(z» + (sum(z) + sum(z»
-c (8(z) + 8(z» + (z * 8(z»
+-Rs/Ls (8(z) * 8(z» + 8(z)

+-Rs/Ls 8(z) * 8(8(z»

for the second critical pair. Again the conjecture is an inductive theorem.

Summary
We have presented an inductive theorem proving method that is based
on the concept of proof by consistency. The essential components of this
method are the computation of covering sets (e.g., via superposition on
inductively complete positions) and a ground reducibility test to check for
inconsistency. We have shown that proof by consistency is complete for dis-
proving inductive theorems when applied to equational theories that can
be represented as ground convergent rewrite systems. The method employs
a linear deduction strategy and has the advantage over full inductive com-
pletion in that it does not fail when it encounters unorientable equations.
The ground convergence of the given theory R, it should be pointed
out, is only needed to prove the refutation completeness of proof by consis-
tency. The same techniques can also be applied to non-convergent sets of
equations. Gramlich (1989, 1990a) formulates a more general proof trans-
formation system for proof by consistency along the lines of ordered com-
pletion. An implementation of a proof by consistency procedure, along with
a number of examples, in particular of theorems arising in the verification
of sorting algorithms, is described in Gramlich (1990b). The relation of
completion-based approaches to (Noetherian) induction has been studied
by Reddy (1990).
Bibliography

[1] ANANTHARAMAN, S., AND HSIANG, J. 1990. Automated proofs of

the Moufang identities in alternative rings. J. Automated Reasoning
6:79-109.
[2] ANANTHARAMAN, S., HSIANG, J., AND MZALI, J. 1989. SbReve2:
A term rewriting laboratory with (AC-)unfailing completion. In Proc.
3rd Int. Con£. on Rewriting Techniques and Applications, Lect. Notes
in Comput. Sci. 355, pp. 533-537. Berlin, Springer-Verlag.
[3] AVENHAUS, J. 1986. On the descriptive power of term rewriting
systems. J. Symbolic Computation 2:109-122.
[4] AVENHAUS, J., AND MADLENER, K. 1990. Term rewriting and
equational reasoning. In Formal Techniques in Artificial Intelligence:
A Source Book, ed. R.B. Banerji. Amsterdam, Elsevier. To appear.
[5] BACHMAIR, L. 1987. Proof methods for equational theories. Ph.D.
diss., University of Illinois, Urbana-Champaign.

[6] BACHMAIR, L. 1988. Proof by consistency in equational theories. In

Proc. Third Annual Symp. Logic in Computer Science, pp. 228-233.
Edinburgh, Scotland.
[7] BACHMAIR, L., AND DERSHOWITZ, N. 1986. Commutation, trans-
formation, and termination. In Proc. 8th Int. Con£. on Automated
Deduction, Lect. Notes in Comput. Sci. 230, pp. 5-20. Berlin,
Springer-Verlag.
[8] BACHMAIR, 1., AND DERSHOWITZ, N. 1987. Inference rules for
rewrite-based first-order theorem proving. In Proc. Second Annual
Symp. on Logic in Computer Science, pp. 331-337. Ithaca, New York.
[9] BACHMAIR, L., AND DERSHOWITZ, N. 1988. Critical pair criteria
for completion. J. Symbolic Computation 6:1-18.

117
118 BIBLIOGRAPHY

[10] BACHMAIR, L., AND DERSHOWITZ, N. 1989. Completion for rewrit-

ing modulo a congruence. Theor. Comput. Sci. 67:173-201.

[11] BACHMAIR, L., DERSHOWITZ, N., AND HSIANG, J. 1986. Orderings

for equational proofs. In Proc. Symp. on Logic in Computer Science,
pp. 346-357. Boston, Massachusetts.

[12] BACHMAIR, L., DERSHOWITZ, N., AND PLAISTED, D. A. 1989.

Completion without failure. In Resolution of Equations in Algebraic
Structures (Vol. 2: Rewriting Techniques), ed. H. Ait-Kaci and M.
Nivat, pp. 1-30. Boston, Academic Press.

[13] BACHMAIR, L., AND GANZINGER, H. 1990. On restrictions of or-

dered paramodulation with simplification. In Proc. 10th Int. ConE. on
Automated Deduction, Lect. Notes in Comput. Sci. 449, pp. 427-44l.
Berlin, Springer-Verlag.

[14] BACHMAIR, 1., AND GANZINGER, H. 1990. Completion of first-

order clauses with equality by strict superposition. In Proc. Second
Int. Workshop on Conditional and Typed Rewriting Systems, Lect.
Notes in Comput. Sci. Berlin, Springer-Verlag. To appear.

[15] BACHMAIR, L., AND PLAISTED, D. A. 1985. Termination orderings

for associative-commutative rewriting systems. J. Symbolic Compu-
tation 1:329-349.

[16] BAIRD, T. B., PETERSON, G. E., AND WILKERSON, R. W. 1989.

Complete sets of reductions modulo associativity, commutativity and
identity. In Proc. 3rd Int ConE. Rewriting Techniques and Applica-
tions, Lect. Notes in Comput. Sci. 355, pp. 29-44. Berlin, Springer-
Verlag.

[17] BEN CHERIFA, A., AND LESCANNE, P. 1987. Termination of rewrit-

ing systems by polynomial interpretations and its implementation.
Sci. Comput. Program. 9:137-159.

[18] BOUDET, A., JOUANNAUD, J.-P., AND SCHMIDT-SCHAUSS, M.

1988. Unification in free extensions of Boolean rings and Abelian
groups. In Proc. Third Annual Symp. on Logic in Computer Science,
pp. 121-130. Edinburgh, Scotland.

[19] BOYER, R. S., AND MOORE, J. S. 1979. A computational logic.

New York, Academic Press.
 BIBLIOGRAPHY 119

[20] BROWN, T.e., JR. 1975. A structured design-method for special-

ized proof procedures. Ph.D. diss., California Institute of Technology,
Pasadena.
[21] BUCHBERGER, B. 1979. A criterion for detecting unnecessary reduc-
tions in the construction of Groebner bases. In Proc. EUROSAM '79,
Lect. Notes in Comput. Sci. 72, pp. 3-21. Berlin, Springer-Verlag.
[22] BUCHBERGER, B. 1984. A critical-pair/completion algorithm for
finitely generated ideals in rings. In Logic and Machines: Decision
Problems and Complexity, Lect. Notes in Comput. Sci. 171, pp. 137-
161. Berlin, Springer-Verlag.
[23] BUCHBERGER, B. 1987. History and basic features of the critical-
pair/completion procedure. J. Symbolic Computation 3:3-38.
[24] BiiNDGEN, R., AND KiicHLIN, W. 1989. Computing ground re-
ducibility and inductively complete positions. In Proc. 3rd Int Conf.
Rewriting Techniques and Applications, Lect. Notes in Comput. Sci.,
pp. 59-75. Berlin, Springer-Verlag.
[25] COMON, H. 1990. Solving inequations in term algebras. In
Proc. Fifth Annual Symp. on Logic in Computer Science, pp. 62-
69. Philadelphia, Pennsylvania.
[26] DERSHOWITZ, N. 1982. Orderings for term-rewriting systems.
Theor. Comput. Sci. 17:279-301.
[27] DERSHOWITZ, N. 1982. Applications of the Knuth-Bendix comple-
tion procedure. In Proc. of the Seminaire d'Informatique Theorique,
pp. 95-111. Paris, France.
[28] DERSHOWITZ, N. 1985. Computing with rewrite systems. Inf. Con-
tro164:122-157.
[29] DERSHOWITZ, N. 1987. Termination ofrewriting. J. Symbolic Com-
putation 3:69-116.
[30] DERSHOWITZ, N. 1989. Completion and its applications. In Reso-
lution of Equations in Algebraic Structures (Vol. 2: Rewriting Tech-
niques), ed. H. Ait-Kaci and M. Nivat, pp. 31-85. Boston, Academic
Press.
[31] DERSHOWITZ, N. 1990. A maximal-literal unit strategy for Horn
clauses. In Proc. Second Int. Workshop on Conditional and Typed
Rewriting Systems, Lect. Notes in Comput. Sci. Berlin, Springer-
Verlag. To appear.
120 BIBLIOGRAPHY

[32] DERSHOWITZ, N., AND JOUANNAUD, J.-P. 1990. Rewrite systems.

In Handbook of Theoretical Computer Science (Vol. B: Formal Mod-
els and Semantics). Amsterdam, North-Holland. To appear.

[33] DERSHOWITZ, N., AND MANNA, Z. 1979. Proving termination with

multiset orderings. Commun. ACM 22:465-476.

[34] DERSHOWITZ, N., AND MARCUS, L. 1985. Existence and construc-

tion of rewrite systems. Unpublished manuscript.

[35] DERSHOWITZ, N., MARCUS, L., AND TARLECKI, A. 1988. Ex-

istence, uniqueness, and construction of rewrite systems. SIAM J.
Comput. 17:629-639.

[36] DEVIE, H. 1990. When ordered completion fails. In Proc. Second

Int. Workshop on Conditional and Typed Rewriting Systems, Lect.
Notes in Comput. Sci. Berlin, Springer-Verlag. To appear.

[37] FAGES, F. 1987. Associative-commutative unification. J. Symbolic

Computation 3:257-275.

[38] FAGES, F., AND HUET, G. 1986. Complete sets of unifiers and
matchers in equational theories. Theor. Comput. Sci. 43:189-200.

[39] FRIBOURG, L. 1985. A superposition oriented theorem prover.

Theor. Comput. Sci. 35:129-164.

[40] FRIBOURG, L. 1989. A strong restriction ofthe inductive completion

procedure. J. Symbolic Computation 8:253-276.

[41] GALLIER, J., AND SNYDER, W. 1989. Complete sets oftransforma-

tions for general E-unification. Theor. Comput. Sci. 67:203-260.

[42] GALLIER, J., AND SNYDER, W. 1990. Designing unification proce-

dures using transformations: A survey. EATCS Bull. 40:273-326'.

[43] GALLIER, J., SNYDER, W., NARENDRAN, P., AND PLAISTED, D. A.

1988. Rigid E-unification is NP-complete. In Proc. Third Annual
Symp. Logic in Computer Science, pp. 218-227. Edinburgh, Scotland.

[44] GALLIER, J., SNYDER, W., AND RAATZ, S. 1989. Rigid E-

unification and its application to equational matings. In Resolution
of Equations in Algebraic Structures (Vol. 1: Algebraic techniques),
pp. 151-216. Boston, Academic Press.
 BIBLIOGRAPHY 121

[45] GANZINGER, H. 1987. A completion procedure for conditional equa-

tions. In Conditional Term Rewriting Systems, Lect. Notes in Com-
put. Sci. 308, pp. 62-83. Berlin, Springer-Verlag. To appear in
J. Symbolic Computation.
[46] GOGUEN, J. A. 1980. How to prove algebraic inductive hypotheses
without induction. In Proc. 5th ConE. Automated Deduction, Lect.
Notes in Comput. Sci. 87, pp. 356-373. Berlin, Springer-Verlag.
[47] GOGUEN, J. A., AND MESEGUER, J. 1986. EQLOG: Equality, types,
and generic modules for logic programming. In Logic Programming:
Functions, Relations, and Equations, ed. D. DeGroot and G. Lind-
strom, pp. 295-363. Englewood Cliffs, Prentice-Hall.
[48] GRAMLICH, B. 1989. Inductive theorem proving using refined unfail-
ing completion techniques. Tech. Rep. SR-89-14, Universitat Kaiser-
slautern, Germany.
[49] GRAMLICH, B. 1990. Completion based inductive theorem proving:
A case study in verifying sorting algorithms. Tech. Rep. SR-90-04,
Universitat Kaiserslautern, Germany.
[50] GRAMLICH, B. 1990. Completion based inductive theorem prov-
ing: An abstract framework and its applications. In Proc. ECAI-90,
pp. 314-319. Stockholm, Sweden.
[51] HENSCHEN, L. J., AND WOS, L. T. 1974. Unit refutations and Horn
clauses. J. ACM 21:590-605.
[52] HSIANG, J. 1985. Refutational theorem proving using term-rewriting
systems. ArtiE. Intell. 25:255-300.
[53] HSIANG, J., AND RUSINOWITCH, M. 1986. A new method for es-
tablishing refutational completeness in theorem proving. In Proc. 8th
Int. ConE. on Automated Deduction, Lect. Notes in Comput. Sci. 230,
pp. 141-152. Berlin, Springer-Verlag.
[54] HSIANG, J., AND RUSINOWITCH, M. 1987. On word problems in
equational theories. In Proc. 14th ICALP, Lect. Notes in Comput.
Sci. 267, pp. 54-71. Berlin, Springer-Verlag.
[55] HUET, G. 1980. Confluent reductions: Abstract properties and ap-
plications to term rewriting systems. J. ACM 27:797-821.
[56] HUET, G. 1981. A complete proof of correctness of the Knuth and
Bendix completion algorithm. J. Comput. Syst. Sci. 23:11-21.
122 BIBLIOGRAPHY

[57] HUET, G., AND HULLOT, J.-M. 1982. Proofs by induction in equa-
tional theories with constructors. J. Comput. Syst. Sci. 25:239-266.
[58] HUET, G., AND QpPEN, D. C. 1980. Equations and rewrite rules:
A survey. In Formal Language Theory: Perspectives and Open Prob-
lems, ed. R. Book, pp. 349-405. New York, Academic Press.
[59] HULLOT, J. 1980. A catalogue of canonical term rewriting systems.
Tech. Rep. CSL-113, SRl International, Menlo Park, California.
[60] JOUANNAUD, J.-P. 1983. Confluent and coherent equational term
rewriting systems: Application to proofs in abstract data types. In
Proc. 8th CoIl. on Trees in Algebra and Programming, Lect. Notes
in Comput. Sci. 59, pp. 269-283. Berlin, Springer-Verlag.
[61] JOUANNAUD, J.-P., AND KIRCHNER, C. 1990. Solving equations
in abstract algebras: A rule-based survey of unification. Tech. Rep.,
Universite de Paris Sud, Orsay.
[62] JOUANNAUD, J.-P., AND KIRCHNER, H. 1986. Completion of a set
of rules modulo a set of equations. SIAM J. Comput. 15:1155-1194.
[63] JOUANNAUD, J.-P., AND KOUNALIS, E. 1986. Automatic proofs by
induction in equational theories without constructors. In Proc. Symp.
Logic in Computer Science, pp. 358-366. Boston, Massachusetts.
[64] JOUANNAUD, J .-P., AND MARCHE, C. 1990. Completion modulo
associativity, commutativity and identity (AC1). In Proc. Int. Symp.
DISCO '90, Lect. Notes in Comput. Sci. 429, pp. 111-120. Berlin,
Springer-Verlag.
[65] KAMIN, S., AND LEVY, J.-J. 1980. Two generalizations of the
recursive path ordering. Univ. of Illinois at Urbana-Champaign. Un-
published manuscript.
[66] KAPUR, D., MUSSER, D. R., AND NARENDRAN, P. 1988. Only
prime superpositions need be considered in the Knuth-Bendix com-
pletion procedure. J. Symbolic Computation 6:19-36.
[67] KAPUR, D., NARENDRAN, P., ROSENKRANTZ, D. J., AND ZHANG,
H. 1987. Sufficient-completeness, quasi-reducibility and their com-
plexity. Tech. Rep., Dept. of Computer Science, SUNY at Albany.
[68] KAPUR, D., NARENDRAN, P., AND ZHANG, H. 1986. Proof by
induction using test sets. In Proc. 8th Int. ConE. on Automated
Deduction, Lect. Notes in Comput. Sci. 230, pp. 99-117. Berlin,
Springer-Verlag. To appear in J. Symbolic Computation.
 BIBLIOGRAPHY 123

[69] KAPUR, D., NARENDRAN, P., AND ZHANG, H. 1987. On sufficient-

completeness and related properties of term rewriting systems. Acta
In£. 24:395-415.

[70] KAPUR, D., AND SIVAKUMAR, G. 1984. Architecture of and experi-

ments with rrl, a rewrite rule laboratory. In Proc. NSF Workshop on
the Rewrite Rule Laboratory, pp. 33-56. Rensellaerville, New York.

[71] KIRCHNER, C. 1986. Computing unification algorithms. In Proc.

Symp. Logic in Computer Science, pp. 206-216. Boston, Mas-
sachusetts.

[72] KIRCHNER, C. 1988. Methods and tools for equational unification.

In Resolution of Equations in Algebraic Structures (Vol. 2: Rewriting
Techniques), ed. H. Ait-Kaci and M. Nivat, pp. 171-210. Boston,
Academic Press.

[73] KLoP, J. W. 1987. Term rewriting systems: A tutorial. Bulletin of

the EATCS 32:143-183.

[74] KLOP, J. W. 1990. Term rewriting systems: From Church-Rosser

to Knuth-Bendix and beyond. In Proc. 17th Int. Colloquium on
Automata, Languages and Programming, Lect. Notes in Comput.
Sci. 443, pp. 350-369. Berlin, Springer-Verlag.

[75] KLoP, J. W. 1990. Thrm rewriting systems. In Handbook of Logic

in Computer Science, ed. S. Abramsky, D. M. Gabbay, and T. S. E.
Maibaum. Oxford, Oxford University Press. To appear.

[76] KNUTH, D. E. 1973. The art of computer programming (Vol. 1:

Fundamental algorithms). Reading, Mass., Addison-Wesley. 2nd edn.

[77] KNUTH, D. E., AND BENDIX, P. B. 1970. Simple word problems in

universal algebras. In Computational Problems in Abstract Algebra,
ed. J. Leech, pp. 263-297. Oxford, Pergamon Press.

[78] KOUNALIS, E., AND RUSINOWITCH, M. 1987. On word problems

in Horn logic. In Proc. First Int. Workshop on Conditional Term
Rewriting, Lect. Notes in Comput. Sci. 204, pp. 390-399. Berlin,
Springer-Verlag.

[79] KUCHLIN, W. 1985. A confluence criterion based on the gener-

alised Newman lemma. In Proc. Eurocal '85, Lect. Notes in Comput.
Sci. 204, pp. 390-399. Berlin, Springer-Verlag.
124 BIBLIOGRAPHY

[80] KUCHLIN, W. 1986. Equational completion by proof simplification.

Tech. Rep. 86-02, Dept. of Mathematics, ETH Ziirich, Switzerland.

[81] KUCHLlN, W. 1986. A generalized Knuth-Bendix algorithm. Tech.

Rep. 86-01, Dept. of Mathematics, ETH Ziirich, Switzerland.

[82] KUCHLlN, W. 1989. Inductive completion by ground proof transfor-

mation. In Resolution of Equations in Algebraic Structures (Vol. 2:
Rewriting Techniques), ed. H. Ait-Kaci and M. Nivat, pp. 211-244.
Boston, Academic Press.

[83] LANKFORD, D. S. 1975. Canonical inference. Tech. Rep. ATP-32,

Dept. of Mathematics and Computer Science, University of Texas,
Austin.
[84] LANKFORD, D. S. 1979. On proving term rewriting systems are
Noetherian. Tech. Rep. MTP-3, Mathematics Department, Louisiana
Tech. Univ., Ruston.

[85] LANKFORD, D. S. 1981. A simple explanation of inductionless in-

duction. Tech. Rep. MTP-14, Mathematics Department, Louisiana
Tech. Univ., Ruston.

[86] LANKFORD, D. S., AND BALLANTYNE, A. M. 1977. Decision proce-

dures for simple equational theories with commutative axioms: Com-
plete sets of commutative reductions. Tech. Rep. ATP-35, Dept. of
Mathematics and Computer Science, University of Texas, Austin.
[87] LANKFORD, D. S., AND BALLANTYNE, A. M. 1977. Decision proce-
dures for simple equational theories with permutative axioms: Canon-
ical sets of permutative reductions. Tech. Rep. ATP-37, Dept. of
Mathematics and Computer Science, University of Texas, Austin.

[88] LANKFORD, D. S., AND BALLANTYNE, A. M. 1977. Decision pro-

cedures for simple equational theories with associative-commutative
axioms: Complete sets of associative-commutative reductions. Tech.
Rep. ATP-39, Dept. of Mathematics and Computer Science, Univer-
sity of Texas, Austin.

[89] LANKFORD, D. S., AND BALLANTYNE, A. M. 1979. The refutation

completeness of blocked permutative narrowing and resolution. In
Proc. Fourth Workshop on Automated Deduction. Austin, Texas.
[90] LE CHENADEC, P. 1986. Canonical forms in finitely presented alge-
bras. New York, Wiley.
 BIBLIOGRAPHY 125

[91] LESCANNE, P. 1983. Computer experiments with the REVE term

rewriting system generator. In Proc. 10th ACM Symp. on Principles
of Programming Languages, pp. 99-108. Austin, Texas.
[92] LESCANNE, P. 1989. Completion procedures as transition rules +
control. In Proc. TAPSOFT '89 (vol. 1), Lect. Notes in Comput.
Sci. 351, pp. 28-41. Berlin, Springer-Verlag.
[93] MARTELLI, A., AND MONTANARI, U. 1982. An efficient unification
algorithm. ACM nans. Program. Lang. Syst. 4:258-282.
[94] MARTIN, U., AND NIPKOW, T. 1990. Ordered rewriting and conflu-
ence. In Proc. 10th Int. Con£. on Automated Deduction, Lect. Notes
in Comput. Sci. 449, pp. 366-380. Berlin, Springer-Verlag.
[95] METIVIER, Y. 1983. About the rewriting systems produced by the
Knuth-Bendix completion algorithm. In£. Process. Lett. 16:31-34.
[96] MUSSER, D. R. 1980. On proving inductive properties of abstract
data types. In Proc. 7th ACM Symp. on Principles of Programming
Languages, pp. 154-162. Las Vegas, Nevada.
[97] MZALI, J. 1986. Methodes de filtrage equationnel et de preuve au-
tomatique de theoremes. Ph.D. diss., Universite de Nancy.
[98] O'DONNELL, M. J. 1985. Equational logic as a programming lan-
guage. Cambridge, Massachusetts, MIT Press.
[99] OHSUGA, A., AND SAKAI, K. 1986. Metis: A term rewriting system
generator. Tech. Rep., ICOT Research Center, Tokyo, Japan.
[100] PATERSON, M. S., AND WEGMAN, M. N. 1978. Linear unification.
J. Comput. Syst. Sci. 16:158-167.
[101] PAUL, E. 1986. On solving the equality problem in theories defined
by Horn clauses. Theor. Comput. Sci. 44:127-153.
[102] PEDERSEN, J. 1984. Confluence methods and the word problem in
universal algebra. Ph.D. diss., Emory University.
[103] PETERSON, G. E. 1983. A technique for establishing completeness
results in theorem proving with equality. SIAM J. Comput. 12:82-
100.
[104] PETERSON, G. E. 1990. Complete sets of reductions with con-
straints. In Proc. 10th Int. Con£. on Automated Deduction, Lect.
Notes in Comput. Sci. 449, pp. 381-395. Berlin, Springer-Verlag.
126 BIBLIOGRAPHY

[105] PETERSON, G. E., AND STICKEL, M. E. 1981. Complete sets of

reductions for some equational theories. J. ACM 28:233-264.

[106] PLAISTED, D. A. 1985. Semantic confluence tests and completion

methods. Inl Control 65:182-215.

[107] PLOTKIN, G. 1972. Building-in equational theories. In Machine

Intelligence 7, ed. B. Meltzer and D. Michie, pp. 73-90. New York,
Wiley.

[108] REDDY, U. 1989. Rewriting techniques for program synthesis. In

Proc. 3rd Int Coni on Rewriting Techniques and Applications, Lect.
Notes in Comput. Sci. 355, pp. 388-403. Berlin, Springer-Verlag.

[109] REDDY, U. 1990. Term rewriting induction. In Proc. 10th Int. Coni
on Automated Deduction, Lect. Notes in Comput. Sci. 449, pp. 162-
177. Berlin, Springer-Verlag.

[110] ROBINSON, G. A., AND WOS, L. T. 1969. Paramodulation and

theorem proving in first order theories with equality. In Machine
Intelligence 4, ed. B. Meltzer and D. Michie, pp. 133-150. New York,
American Elsevier.

[111] ROBINSON, J. A. 1965. A machine-oriented logic based on the reso-

lution principle. J. ACM 12:23-41.

[112] RUSINOWITCH, M. 1991. Theorem proving with resolution and su-

perposition: An extension of the Knuth and Bendix procedure as a
complete set of inference rules. J. Symbolic Computation. To appear.

[113] SIEKMAN, J. 1984. Universal unification. In Proc. 7th Int. Coni

on Automated Deduction, Lect. Notes in Comput. Sci. 170, pp. 1-42.
Berlin, Springer-Verlag.

[114] SLAGLE, J. R. 1974. Automated theorem proving for theories with

simplifiers, commutativity, and associativity. J. ACM 21:622-642.

[115] STICKEL, M. E. 1981. A unification algorithm for associative-

commutative functions. J. ACM 28:423-434.

[116] WINKLER, F. 1984. The Church-Rosser property in computer

algebra and special theorem proving: An investigation of critical-
pair/completion algorithms. Ph.D. diss., Johannes Kepler University,
Linz, Austria.
 BIBLIOGRAPHY 127

[117] WINKLER, F. 1985. Reducing the complexity of the Knuth-Bendix

completion algorithm: A 'unification' of different approaches. In
Proc. Eurocal '85, Lect. Notes in Comput. Sci. 204, pp. 378-389.
Berlin, Springer-Verlag.
[118] WINKLER, F., AND BUCHBERGER, B. 1983. A criterion for elim-
inating unnecesssary reductions in the Knuth-Bendix algorithm. In
Proc. CoIl. on Algebra, Combinatorics and Logic in Computer Sci-
ence. Gyor, Hungary.
[119] ZHANG, H., AND KAPUR, D. 1989. Consider only general superpo-
sitions in completion procedures. In Proc. 3rd Int Conf. on Rewrit-
ing Techniques and Applications, Lect. Notes in Comput. Sci. 355,
pp. 513-527. Berlin, Springer-Verlag.
Index

Anantharaman, Siva, 91, 117 Boyer, Robert S., 111, 118

Associative-commutative comple- Brown, Thomas Carl, Jr., 90, 119
tion, 60-63 Buchberger, Bruno, viii, 3, 33n,
Atomic formula, 91 34, 119, 127
Avenhaus, Jiirgen, viii, 4,74,117 Biindgen, Reinhard, 112, 119
Axioms: Church-Rosser property, 7, 24-
associativity, 39, 41, 53-54, 25,32
60-64, 81, 83, 99, 113 modulo a set of equations,
commutativity, 39, 41, 54, 41, 42, 45, 47, 51
60-64,73,75,81,83,99, Clause, 91
113 Horn, 92
distributivity, 113 positive unit, 92
equipotency, 68 redundant, 95
idempotency, 83 subsumed, 95
identity, 68 Cliff, 42, 47-48
Bachmair, Leo, viii, 36, 41, 46, Comon, Hubert, 80, 119
64, 69, 91, 95, 98, 117, Compatibility of reduction order-
118 ings, 41, 101
Baird, Timothy B., 71, 118 Completion procedure, basic or
Ballantyne, A. M., 33, 40, 124 standard, 15, 24, 28-29
Basic Completion, 14-24 Completion procedure, extended,
correctness, 24 55,60,67
fairness, 24 Completion procedure, ordered,
inference system, 14 78
normal-form proofs, 20 Compositeness, 35-38
proof ordering, 19 Congruence class, 40
soundness, 15 Congruence relation, 6
Ben Cherifa, Ahlem, 64, 119 Connectedness, 33-34
Bendix, Peter B., 2, 13, 19, 21, Consistency, 99-100
30,74, 123 Constant, 5
Bonacina, Maria-Paola, viii Convergence, 7, 25
Book, Ronald V., viii ground, 75, 79,81,85, 95,99
Boudet, Alexandre, 98, 118 modulo a set of equations,

129
130 INDEX

41, 68 labelled, 10, IOn

modulo associativity and orientable instance of, 75
commutativity, 62 permutative, 39, 78
on a set of equations, 24 persisting, 14
Correctness, of completion proce- Equational proof, see Proof
dure, 13, 15, 24, 28, 55 Equational theory, 7
Covering set, 109, 110, 111-113 ground, 82
Critical overlap, see under Over- Equivalence of terms, 7
lap Equivalence relation, 6n
Critical pair, 21 Extended completion, see
complete set of, 37 Extended rule method,
modulo a set of equations, Left-linear rule method,
49-50 Protected rule method
ordered, 79-80 Extended rewriting, 40-41
subsumed, 37 Extended rule, 53, 61
Critical pair criteria: Extended rule method, 55-60
Composite, 35 correctness, 60
Connected, 34 fairness, 59
Extended, 69-70 inference system, 54-55
Non-blocked, 33 normal-form proofs, 47
Critical pair criterion, 32 proof ordering, 57-58
correctness of, 32 soundness, 55
soundness of, 32 Fages, Francois, 49, 120
fairness with respect to, 32 Failure, of completion procedure,
Critical Pair Lemma, 21 15,55
Extended, 50 Fairness, 20, 24, 28, 46, 59, 67,
Ordered, 80 80, 85, 95, 109
Critical pair position, 21, 79 with respect to a critical pair
Critical pair proof, 21 criterion, 32
Derivation, 14 Fribourg, Laurent, 91, 101, 105,
failing, 15, 73 106, 111, 112, 120
limit of, 14 Function symbol, 5
non-failing, 15 arity of, 5
simplifying, 29 constructor, 101, 105, 112
Dershowitz, Nachum, viii, 4, 8, 9, status of, 8
24n, 28, 30, 35, 36, 46, lexicographic, 8
64, 69, 73, 90, 98, 99, multiset, 8
100, 105, 117, 118, 119, Gallier, Jean, viii, 49, 98, 120
120 Ganzinger, Harald, viii, 31, 35,
Devie, Herve, 88, 120 91, 95, 118, 121
Equality step, 13 Goguen, Joseph A., 1, 99, 121
Equation, 6 Gramlich, Bernhard, 115, 121
 INDEX 131

Ground reducibility, Orientation, 14, 54, 77

of term, 100 Paramodulation, 94
of equation, 101 Protection, 54
Group, Resolution, 94
Abelian, 63-64, 83 Simplification, 14, 54, 77, 95,
free, 2, 17-19 104
left, 30 Subsumption, 31, 94
Groupoid, Inference systems:
central, 30 Basic completion, 14
entropic, 78 Extended completion, 54-55
Henschen, L. J., 93, 121 Left-linear completion, 43
Herbrand base, 91 Ordered completion, 76
Herbrand interpretation, see In- for Horn clauses, 94
terpretation Proof by consffitency, 104
Herbrand model, see Model Standard completion, 26, 77
Herbrand universe, 91 Unfailing completion, 84
Hermann, Miki, viii Initial model, 99, 99n
Hsiang, Jieh, viii, 46, 64, 78, 91, Instance of a term, 6
91n, 117, 118, 121 modulo a set of equations, 40
Huet, Gerard, 4, 28, 31, 35, 39, proper, 6
41, 45, 49, 71, 101, 105, Interpretation, 92
112, 120, 121, 122 equality, 92
Hullot, Jean-Marie, 63, 101, 105, Irreducibility, 7, 8
112, 122 Jouannaud, Jean-Pierre, viii, 4,6,
Inconsffitency, 100 40,50,51,53,65,68,69,
provable, 102, 110, 111 71, 98, 100, 101, lOIn,
Inductive completion procedure, 102, 105, 106, 107n, 118,
105-106 120, 122
Inductive theorem, 99, 105n, 108 Kamin, Sam, 9, 122
examples of, 113-115 Kapur, Deepak, 30, 32, 33n, 36,
Inference rule, 13 37,38,70,101,105,106,
Inference rules: 122, 123, 127
Collapse, 26, 54, 65, 78 Kirchner, Claude, 6, 49, 122, 123
Composition, 26, 54, 77 Kirchner, Helene, 40, 51, 53, 65,
Conversion, 94 68, 69, 71, 122
Deduction, 14,43,54, 76, 77, Klop, Jan Willem, In, 4, 123
83, 84, 94, 104 Knuth, Donald Ervin, 2, 13, 19,
Deletion, 14, 31, 43, 54, 76, 21, 25, 30, 74, 123
77, 83, 94, 104 Kounalis, Emmanuel, 98, 100,
Extension, 54 101, lOIn, 102, 105, 106,
Factoring, 93 122, 123
Induction, 104 Kiichlin, Wolfgang, 34, 35, 35n,
132 INDEX

37, 70, 106, 112, 119, Narendran, Paliath, 36, 37, 70,
123, 124 98, 101, 105, 106, 120,
Label of an equation, 10, lOn, 13, 122, 123
42, 54, 76, 104 Nipkow, Tobias, 80, 81, 83, 125
Lankford, Dallas S., 33, 40, 64, Non-overlap, 21-22, 48
80, 82, 90, 105, 124 Normal form, proof, 16
Le Chenadec, Philippe, 30, 124 Normal form, term, 7
Left-linear rule method, 42-46 ground,75
correctness, 46 O'Donnell, Michael J., 1, 125
fairness, 46 Ohsuga, Akihiko, 91, 125
inference system, 43 Oppen, Derek C., 4, 122
normal-form proofs, 45 Ordered completion, 75-83
proof ordering, 44 correctness, 81
soundness, 44 fairness, 80
Lescanne, Pierre, viii, 30, 64, 118, inference system, 76
125 normal-form proofs, 79
Levy, Jean-Jacques, 9, 122 proof ordering, 76
Lexicographic path ordering, 9, soundness, 76
82, 85 Ordering, 7
Lifting Lemma, 96 encompassment, 26
Linearity, of proof by consistency, modulo a set of equations,
105 50
Literal similarity, 6, 86 lexicographic combination,
Madlener, Klaus, 4, 117 7,8
Manna, Zohar, 8, 120 multiset, 8
Marche, Claude, 71, 122 polynomial, 82
Marcus, Leo, 73, 90, 120 subterm, 108n
Martelli, A., 6, 125 modulo a set of equations,
Martin, Ursula, 81, 83, 125 50-51
Matching, 6 Overlap, 21
modulo a set of equations, 40 blocked, 33, 70
Meseguer, Jose, 1, 121 critical, 21, 79
Metivier, Yves, 7, 125 modulo a set of equations,
Model,92 50
equality, 92 extended, 48
Montanari, Ugo, 6, 125 non-blocked, 33-34, 70
Moore, J. Strother, 111, 118 prime critical, 36
Multiset,8 proper, 22-23, 48
Multiset path ordering, 9 variable, 22-23, 42-43, 48
Musser, David R., 36, 37, 70,105, Overlapped term, 21, 79
122, 125 Paramodulation, 93
Mzali, Jalel, 91, 117, 125 ordered positive unit, 93
 INDEX 133

Paterson, M. S., 6, 125 Proof step, 10

Paul, Etienne, 98, 125 blocked, 70
Peak, 10,21,42,47-48 bound, 51, 57
composite, 35 cost of, see Proof complexity
decomposition of, 35 variable part of, 50
Pedersen, John, 79, 125 Prooftransformation relation, 11,
Peterson, Gerald E., 39, 40, 53, 16, 27,44
55,61,62,63,64,71,83, Proof transformation rule, 16
90, 96, 118, 125, 126 Proof transformation rules:
Plaisted, David A., viii, 41, 64, for collapse, 26-27, 56, 65
98, 101, 118, 120, 126 for composition, 26-27, 56
Plotkin, Gordon, 49, 126 for deduction, 16-17, 44
Position in a term, 5 for deletion, 16-17, 44, 56
inductively complete, 111 for extension, 56
Precedence ordering, 8 for non-overlap, 48
Predicate symbol, 91 for orientation, 16-17, 17, 56
Proof, 10 for protection, 56
composition, 11 for simplification, 16-17, 17,
ground, 11 56
inverse, 10 for variable overlap, 48-49
Proof by consistency, 103-111 Proof transformation step, 16
fairness, 109 Proof transformation system, 16
inference system, 104 Proof transformation systems:
normal-form proofs, 107 for basic completion, 16, 19
proof ordering, 108 for extended completion, 56-
refutation completeness, 107 57
soundness, 105 for left-linear completion, 44
Proof complexity, 19, 27, 44, 51- for standard completion, 27
52, 57-58, 66, 76, 108 Protected rule method, 65-69
Proof ordering, 11 correctness, 68
Proof orderings: fairness, 67
for basic completion, 19 inference system, 65
for extended completion, 57- normal-form proofs, 47
58, 66 proof ordering, 66
for left-linear completion, 44 soundness, 55
for ordered completion, 76 Quasi-ordering, 7
for proof by consistency, 108 strict part of, 7
for standard completion, 27 Raatz, Stan, 98, 120
Proof reduction ordering, see Recursive path ordering, 9
Proof ordering Reddy, Uday, viii, 98, 115, 126
Proof rewrite relation, 11 Reduction ordering, 8
Proof simplification, 19, 103 completable, 79, 88, 89
134 INDEX

complete, 79, 85, 88, 94 Rusinowitch, Michael, viii, 78, 91,

Reduction sequence, 88 91n, 98, 121, 123, 126
innermost, 88 Sakai, Ko, 91, 125
Reflection, 16, 26-27, 44, 57, 76 Satisfiability, 92
Refutation completeness, 96, 107 Schmidt-SchauB, Manfred, 98,
Refutational theorem proving, 118
90-91,107 Semi-critical pair, 85
Remy, Jean-Luc, viii Siekmann, Jorg, 49, 126
Resolution, 92 Simplification ordering, 8
ordered positive unit, 93 Sivakumar, G., viii, 30, 123
Rewrite ordering, 8 Skolem constant, 86, 90
Rewrite proof, 10, 20 Slagle, James R., 33, 70, 126
ground,79 Snyder, Wayne, viii, 49, 98, 120
modulo a set of equations, Soundness, 15, 26, 44, 55, 76, 95,
42,47 105
Rewrite relation, 6 Standard completion, 25-31
Rewrite rule, 7, 13 correctness, 28
protected, 54 fairness, 28
unprotected, 54 inference system, 26
normal-form proofs, 20
Rewrite step, 13
proof ordering, 27
Rewrite system, 7
soundness, 26
canonical, 7
Stickel, Mark E., 39, 40, 49, 53,
Church-Rosser, 24, 37
55, 61, 62, 63, 64, 71,
convergent, 7, 24 126
non-overlapping, 25 Subproof, 11
reduced, 7, 68 replacement, 11
terminating, 15 Substitution, 5
Rewrite systems: composition of, 5
for Ackermann's function, 2 irreducible, 102
for symbolic differentiation, Subterm,5
25 proper, 5
for combinatory logic, 15 property, 8
Rewriting, 6-7 replacement, 5
Rewriting modulo a congruence, Success, of completion procedure,
see Extended rewriting 15,78
Ring, Sufficient completeness, 105
Associative-commutative, 64 Superposition, 21, 79
Boolean, 64, 84 Tarlecki, Andrzej, 73, 120
Robinson, G. A., 75, 90, 126 Tautology, 92
Robinson, J. A., 6, 126 Term, 5
Rosenkrantz, Daniel J., 101, 122 ground,5
 INDEX 135

Termination, 7
Transfinite semantic tree method,
91
Transformation relation, see
Proof transformation re-
lation
Unfailing completion, 84-85
Unification, 6
modulo a set of equations, 49
Unifier, 6
complete set of, 49
minimal set of, 49
most general, 6
Unsatisfiability, 92
Variable, 5
Wegman, M. N., 6,125
Well-foundedness, 7
Wilkerson, Ralph W., 71, 118
Winkler, Franz, 33n, 34, 35, 35n,
69, 126, 127
Wos, L. T., 75, 90, 93, 121, 126
Zhang, Hantao, 32, 33n, 38, 101,
105, 106, 122, 123, 127
Progress in Theoretical Computer Science
Editor
Ronald V. Book
Department of Mathematics
University of California
SantaBarbara, CA 93106

Editorial Board
Erwin Engeler Robin Milner
Mathematik Department of Computer Science
ETHZentrum University of Edinburgh
CH-8092 Zurich, Switzerland Edinburgh EH9 3JZ, Scotland

Gerard Huet Maurice Nivat

INRIA Universite de Paris VII
Domaine de Voluceau-Rocquencourt 2, place lussieu
B. P.105 75251 Paris Cedex 05
78150 Le Chesnay Cedex, France France

lean-Pierre louannaud Martin Wirsing

Laboratoire de Recherche Universitiit Passau
en Informatique Bat. 490 Fakultlit fUr Mathematik
Universite de Paris-Sud und Informatik
Centre d'Orsay Postfach 2540
91405 Orsay Cedex, France D-8390 Passau, Germany

Progress in Theoretical Computer Science is a series that focuses on the theoretical aspects
of computer science and on the logical and mathematical foundations of computer science,
as well as the applications of computer theory. It addresses itself to research workers and
graduate students in computer and information science departments and research labora-
tories, as well as to departments of mathematics and electrical engineering where an interest
in computer theory is found.

The series publishes research monographs, graduate texts, and polished lectures from
seminars and lecture series. We encourage preparation of manuscripts in some form of TeX
for delivery in camera-ready copy, which leads to rapid publication, or in electronic form for
interfacing with laser printers or typesetters.

Proposals should be sent directly to the Editor, any member of the Editorial Board, or to:
Birkhiiuser Boston, 675 Massachusetts Avenue, Cambridge, MA 02139.