SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Abstract Congruence Closure and Specializations
 by Dr. Ashish Tiwari & Leo Bachmair.

Lecture Notes in Artificial Intelligence, Volume 1831.
From Automated Deduction CADE-17.
Edited by David McAllester.
Springer-Verlag, Pittsburgh, PA.
June, 2000.
Pages 64–78.

We use the uniform framework of abstract congruence closure to study the congruence closure algorithms described by Nelson and Oppen, Downey, Sethi and Tarjan and Shostak. 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 standard completion enhanced with an extension rule that enlarges a given signature by new constants.
BibTEX Entry
    AUTHOR = {Leo Bachmair and Ashish Tiwari},
    TITLE = {Abstract Congruence Closure and Specializations},
    BOOKTITLE = {Automated Deduction --- {CADE-17}},
    YEAR = {2000},
    EDITOR = {David McAllester},
    SERIES = {Lecture Notes in Artificial Intelligence},
    VOLUME = {1831},
    PAGES = {64--78},
    ADDRESS = {Pittsburgh, {PA}},
    MONTH = {jun},
    PUBLISHER = {Springer-Verlag},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy