Congruence Closure Modulo Associativity and Commutativity

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

Presented at Workshop on Frontiers of Combining Systems, FroCoS 2000 , Nancy, France, March 2000. © Springer-Verlag. The final version will be available at the Springer LNCS site

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