Lecture Notes in Artificial Intelligence, Volume 1794.
From Frontiers of Combining Systems, 3rd Intl Workshop FroCoS 2000.
Edited by H. Kirchner, and C. Ringeissen.
Springer-Verlag, Nancy, France.
March, 2000.
Pages 245–259.

We introduce the notion of an 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.

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

• frocos00.ps.gz