On the Combination of Congruence Closure and Completion - Artificial Intelligence and Symbolic Computation - page 103

On the Combination
of Congruence Closure and Completion

Christelle Scharff 1 , and Leo Bachmair 2

1 Department of Computer Science, Pace University, NY, USA
[e-mail]
2 Department of Computer Science, SUNY Stony Brook, NY, USA
[e-mail]

Abstract. We present a graph-based method for constructing a con-
gruence closure of a given set of ground equalities that combines the key
ideas of two well-known approaches, completion and abstract congruence
closure, in a natural way by relying on a specialized and optimized ver-
sion of the more general, but less ecient, SOUR graphs. This approach
allows for ecient implementations and a visual presentation that bet-
ter illuminates the basic ideas underlying the construction of congruence
closures and clarifies the role of original and extended signatures and the
impact of rewrite techniques for ordering equalities.

1 Introduction

Theories presented by finite sets of ground (i.e., variable-free) equalities are
known to be decidable. A variety of different methods for solving word problems
for ground equational theories have been proposed, including algorithms based
on the computation of a congruence closure of a given relation. Ecient con-
gruence closure algorithms have been described in [5, 8, 10, 12]. These algorithms
typically depend on sophisticated, graph-based data structures for representing
terms and congruence relations.
A different approach to dealing with ground equational theories is represented
by term rewriting [1, 4], especially the completion method [7] for transforming a
given set of equalities into a convergent set of directed rules that defines unique
normal forms for equal terms and hence provides a decision procedure for the
word problem of the underlying equational theory. Completion itself is a semi-
decision procedure but under certain reasonable assumptions about the strategy
used to transform equalities, is guaranteed to terminate if the input is a set of
ground equalities. Completion methods are not as ecient as congruence closure,
though an ecient ground completion method has been described by [13], who
obtains an O ( nlog ( n )) algorithm that cleverly uses congruence closure to trans-
form a given set of ground equalities into a convergent ground rewrite system.
Standard completion is quadratic in the worst case [11].