@inproceedings{4ca3fe8c1acf449ebd61f1967d2374f9,
title = "Congruence closure modulo associativity and commutativity?",
abstract = "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.",
author = "L. Bachmair and Ramakrishnan, \{I. V.\} and A. Tiwari and L. Vigneron",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 3rd International Workshop on Frontiers of Combining Systems, FroCoS 2000 ; Conference date: 22-03-2000 Through 24-03-2000",
year = "2000",
doi = "10.1007/10720084\_16",
language = "English",
isbn = "9783540672814",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "245--259",
editor = "Helene Kirchner and Christophe Ringeissen",
booktitle = "Frontiers of Combining Systems - 3rd International Workshop, FroCoS 2000, Proceedings",
}