**
Congruence Closure Modulo Associativity and Commutativity
**

###
L. Bachmair, I. V. Ramakrishnan, A. Tiwari and L. Vigneron

### Abstract

We introduce the notion of an {\em associative-commutative
congruence closure}
and show how such closures can be constructed via
completion-like transition rules.
This method is based on combining completion algorithms
for theories over disjoint signatures to produce a
convergent rewrite system over an extended signature.
This approach can also be used to solve the word problem
for ground $AC$-theories without the need for $AC$-simplification
orderings total on ground terms.
Associative-commutative congruence closure provides a novel way
to construct a convergent rewrite system for a ground $AC$-theory. This is
done by transforming an $AC$-congruence closure, which is
described by rewrite rules
over an extended signature, to a rewrite system over the original
signature. The set of rewrite rules thus obtained is convergent
with respect to
a new and simpler notion of associative-commutative reduction.
gzipped postscript or
postscript

#### BibTeX Entry

@inproceedings{BRTV00:FroCoS,
TITLE = {Congruence Closure Modulo Associativity and Commutativity},
AUTHOR = {L. Bachmair and I.V.Ramakrishnan and A. Tiwari and L. Vigneron},
BOOKTITLE = {Frontiers of Combining Systems, 3rd Intl
Workshop FroCoS 2000},
EDITOR = {Kirchner, H. and Ringeissen, C.},
PAGES = {245--259},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1794,
MONTH = mar,
YEAR = 2000,
ADDRESS = {Nancy, France}
}

Return to the **Formal Methods Program** home page

Return to the **Computer Science Laboratory** home page