Congruence Closure Modulo Associativity and Commutativity

### 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.

#### 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,