Abstract Congruence Closure and Specializations

### 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.

#### BibTeX Entry


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,