Abstract
We use the uniform framework of abstract congruence closure to study the congruence closure algorithms described by Nelson and Oppen [9], Downey, Sethi and Tarjan [7], and Shostak [11]. The descriptions thus obtained abstract 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.
The research described in this paper was supported in part by the National Science Foundation under grant CCR-9902031.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. J. ACM 41, 236–276 (1994)
Bachmair, L., Ramakrishnan, C., Ramakrishnan, I., Tiwari, A.: Normalization via rewrite closures. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 190–204. Springer, Heidelberg (1999)
Bachmair, L., Ramakrishnan, I., Tiwari, A., Vigneron, L.: Congruence closure modulo associativity and commutativity. In: Kirchner, H., Ringeissen, C. (eds.) FroCos 2000. LNCS (LNAI), vol. 1794, pp. 245–259. Springer, Heidelberg (2000)
Chew, L.P.: Normal forms in term rewriting systems. PhD thesis. Purdue University (1981)
Clavel, M., et al.: Maude: Specification and Programming in Rewriting Logic. SRI International, Menlo Park, CA (1999), http://maude.csl.sri.com/manual/
Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, North-Holland, Amsterdam (1990)
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. ACM 27(4), 758–771 (1980)
Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23–37. Springer, Heidelberg (1997)
Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)
Plaisted, D., Sattler-Klein, A.: Proof lengths for equational completion. Information and Computation 125, 154–170 (1996)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 21(7), 583–585 (1984)
Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. Journal of Symbolic Computation 15(7) (1993)
Tiwari, A., Bachmair, L., Ruess, H.: Rigid E-unification revisited. In: McAllester, D. (ed.) 17th Intl Conf. on Automated Deduction, CADE-17 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmair, L., Tiwari, A. (2000). Abstract Congruence Closure and Specializations. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_5
Download citation
DOI: https://doi.org/10.1007/10721959_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive