
Congruence Closure Modulo Associativity and Commutativity
by Dr. Ashish Tiwari, L. Bachmair, I.V.Ramakrishnan & L. Vigneron.
Lecture Notes in Artificial Intelligence, Volume 1794. From Frontiers of Combining Systems, 3rd Intl Workshop FroCoS 2000. Edited by H. Kirchner, and C. Ringeissen. SpringerVerlag, Nancy, France. March, 2000. Pages 245–259.
Abstract
We introduce the notion of an associativecommutative congruence closure and show how such closures can be constructed via completionlike 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 ACtheories without the need for ACsimplification orderings total on ground terms. Associativecommutative congruence closure provides a novel way to construct a convergent rewrite system for a ground ACtheory. This is done by transforming an ACcongruence 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 associativecommutative reduction.
BibT_{E}X Entry
@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 = {245259},
ADDRESS = {Nancy, France},
MONTH = {mar},
PUBLISHER = {SpringerVerlag},
URL = {http://www.csl.sri.com/papers/frocos00/}
}
Files

