Abstract Congruence Closure and Specializations
Leo Bachmair and Ashish Tiwari
Presented at
CADE'00, Pittsburgh, PA, June 2000.
© Springer-Verlag. The final version will be available at
the Springer LNCS site
Abstract
We use the uniform framework of {\em abstract
congruence closure} to study the
congruence closure algorithms described by
Nelson and Oppen~\cite{NO-jacm-80},
Downey, Sethi and Tarjan~\cite{DST-jacm-80}
and Shostak~\cite{Shostak-84}.
The descriptions thus obtained abstracts from certain implementation
details while still allowing for comparison between these
different algorithms. Experimental results are presented to
illustrate the relative efficiency and explain
differences in performance
of these three algorithms.
The transition rules for computation of abstract
congruence closure are obtained from rules
for {\em standard completion\/} enhanced with an
{\em extension\/} rule that enlarges a given signature by
new constants.
Errata: The text following the regular expression describing Shostak's congruence
closure algorithm is not entirely correct.
In particular, Simplification must be used eagerly, after every application of
Extension. For example, a term fbb in E should result in just two D-rules,
b -> c0 and fc0c0 -> c1.
gzipped postscript or
postscript
BibTeX Entry
@inproceedings{BachmairTiwari00:CADE,
TITLE = {Abstract Congruence Closure and Specializations},
AUTHOR = {Leo Bachmair and Ashish Tiwari},
BOOKTITLE = {Conference on Automated Deduction, CADE '2000},
EDITOR = {David McAllester},
PAGES = {64--78},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = 1831,
MONTH = jun,
YEAR = 2000,
ADDRESS = {Pittsburgh, PA}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page