Abstract
We introduce the notion of an associative-commutative congruence closure and show how such closures can be constructed via completion-like transition rules. This method is based on combining completion algorithms for theories over disjoint signatures to produce a convergent rewrite system over an extended signature. This approach can also be used to solve the word problem for ground AC-theories without the need for AC-simplification orderings total on ground terms.
Associative-commutative congruence closure provides a novel way to construct a convergent rewrite system for a ground AC-theory. This is done by transforming an AC-congruence closure, which is described by rewrite rules over an extended signature, to a rewrite system over the original signature. The set of rewrite rules thus obtained is convergent with respect to a new and simpler notion of associative-commutative reduction.
The research described in this paper was supported in part by the National Science Foundation under grants CCR-9902031, CCR-9711386 and EIA-9705998.
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.: Canonical Equational Proofs. Birkhäuser, Boston (1991)
Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theoretical Computer Science 67(2 & 3), 173–201 (1989)
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)
Ballantyne, A.M., Lankford, D.S.: New decision algorithms for finitely presented commutative semigroups. Comp. and Maths. with Appls. 7, 159–165 (1981)
Becker, T., Weispfenning, V.: Gröbner bases: a computational approach to commutative algebra. Springer, Berlin (1993)
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)
Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)
Domenjoud, E., Klay, F.: Shallow AC theories. In: Proceedings of the 2nd CCL Workshop, La Escala, Spain (September 1993)
Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23–37. Springer, Heidelberg (1997)
Koppenhagen, U., Mayr, E.W.: An optimal algorithm for constructing the reduced Gröbner basis of binomial ideals. In: Lakshman, Y.D. (ed.) Proceedings of the International Symposium on Symbolic and Algebraic Computation, pp. 55–62 (1996)
Marche, C.: On ground AC-completion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 411–422. Springer, Heidelberg (1991)
Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics 46, 305–329 (1982)
Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 423–434. Springer, Heidelberg (1991)
Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. Journal ofthe Association for Computing Machinery 27(2), 356–364 (1980)
Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981)
Ringeissen, C.: Cooperation of decision procedures for the satisfiability problem. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, pp. 121–139. Kluwer Academic Publishers, Dordrecht (1996)
Rubio, A., Nieuwenhuis, R.: A precedence-based total AC-compatible ordering. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 374–388. Springer, Heidelberg (1993)
Tinelli, C., Harandi, M.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, pp. 103–119. Kluwer Academic Publishers, Dordrecht (1996)
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., Ramakrishnan, I.V., Tiwari, A., Vigneron, L. (2000). Congruence Closure Modulo Associativity and Commutativity. In: Kirchner, H., Ringeissen, C. (eds) Frontiers of Combining Systems. FroCoS 2000. Lecture Notes in Computer Science(), vol 1794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720084_16
Download citation
DOI: https://doi.org/10.1007/10720084_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67281-4
Online ISBN: 978-3-540-46421-1
eBook Packages: Springer Book Archive