We present a graph-based method for constructing a congruence closure of a given set of ground equalities that combines the key ideas of two well-known approaches, completion and abstract congruence closure, in a natural way by relying on a specialized and optimized version of the more general, but less efficient, SOUR graphs. This approach allows for efficient implementations and a visual presentation that better illuminates the basic ideas underlying the construction of congruence closures and clarifies the role of original and extended signatures and the impact of rewrite techniques for ordering equalities. © Springer-Verlag 2004.
CITATION STYLE
Scharff, C., & Bachmair, L. (2004). On the Combination of Congruence Closure and Completion. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3249, 103–117. https://doi.org/10.1007/978-3-540-30210-0_10
Mendeley helps you to discover research relevant for your work.