Abstract Congruence Closure
Leo Bachmair, Ashish Tiwari, and Laurent Vigneron
In the Journal of Automated Reasoning 31(2), 2003.
Abstract
We describe the concept of an {\em abstract congruence closure}
and provide equational inference rules for its construction.
The length of any maximal derivation using these inference rules
for constructing an abstract congruence closure
is at most quadratic in the input size.
The framework is used to describe the logical
aspects of some well-known algorithms for congruence closure.
It is also used to obtain an efficient implementation of congruence
closure. We present experimental results that illustrate the
relative differences in performance of the different algorithms.
The notion is extended to handle associative and commutative function
symbols, thus providing the concept of an {\em associative-commutative
congruence closure}. Congruence closure (modulo associativity and
commutativity) can be used to construct
ground convergent rewrite systems corresponding to a set of ground
equations (containing $AC$ symbols).
BibTeX Entry
@article{BachmairTiwariVigneron03:JAR,
TITLE = {Abstract congruence closure},
AUTHOR = {Leo Bachmair and Ashish Tiwari and Laurent Vigneron},
JOURNAL = {J. of Automated Reasoning},
PAGES = {129--168},
PUBLISHER = {Kluwer Academic Publishers},
VOLUME = 31,
NUMBER = 2,
YEAR = 2003,
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page