|
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. Springer-Verlag, Nancy, France. March, 2000. Pages 245259.
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.
BibTEX 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 = {245--259},
ADDRESS = {Nancy, France},
MONTH = {mar},
PUBLISHER = {Springer-Verlag},
URL = {http://www.csl.sri.com/papers/frocos00/}
}
Files
|
|