Document Open Access Logo

A Modular Associative Commutative (AC) Congruence Closure Algorithm

Author Deepak Kapur

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.15.pdf
  • Filesize: 0.67 MB
  • 21 pages

Document Identifiers

Author Details

Deepak Kapur
  • Department of Computer Science, University of New Mexico, Albuquerque, NM, USA

Funding

Research partially supported by the NSF award: CCF-1908804.

Acknowledgements

Heartfelt thanks to the referees for their reports which substantially improved the presentation.

Cite AsGet BibTex

Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.15

Abstract

Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.

Subject Classification

ACM Subject Classification
  • Software and its engineering
  • Theory of computation
  • Mathematics of computing
Keywords
  • Congruence Closure
  • Associative and Commutative
  • Word Problems
  • Finitely Presented Algebras
  • Equational Theories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Franz Baader and Deepak Kapur. Deciding the word problem for ground identities with commutative and extensional symbols. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 163-180. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_10.
  2. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. J. Symb. Comput., 6(1):1-18, 1988. URL: https://doi.org/10.1016/S0747-7171(88)80018-X.
  4. Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, and Laurent Vigneron. Congruence closure modulo associativity and commutativity. In Hélène Kirchner and Christophe Ringeissen, editors, Frontiers of Combining Systems, Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000, Proceedings, volume 1794 of Lecture Notes in Computer Science, pages 245-259. Springer, 2000. URL: https://doi.org/10.1007/10720084_16.
  5. Leo Bachmair, Ashish Tiwari, and Laurent Vigneron. Abstract congruence closure. J. Autom. Reason., 31(2):129-168, 2003. URL: https://doi.org/10.1023/B:JARS.0000009518.26415.49.
  6. A. Michael Ballantyne and Dallas Lankford. New decision algorithms for finitely presented commutative semigroups. Computers and Mathematics Applications, 7:159-165, 1981. Google Scholar
  7. Thomas Becker, Volker Weispfenning, and Heinz Kredel. Gröbner bases - a computational approach to commutative algebra, volume 141 of Graduate texts in mathematics. Springer, 1993. Google Scholar
  8. Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. Variations on the common subexpression problem. J. ACM, 27(4):758-771, 1980. URL: https://doi.org/10.1145/322217.322228.
  9. Abdelilah Kandri-Rody and Deepak Kapur. On relationship between buchberger’s gröbner basis algorithm and the knuth-bendix completion procedure. Technical report no. ge-83crd286, General Electric Corporate Research and Development, Schenectady, NY, November 1983. Google Scholar
  10. Abdelilah Kandri-Rody and Deepak Kapur. Computing a gröbner basis of a polynomial ideal over a euclidean domain. J. Symb. Comput., 6(1):37-57, 1988. URL: https://doi.org/10.1016/S0747-7171(88)80020-8.
  11. Abdelilah Kandri-Rody, Deepak Kapur, and Paliath Narendran. An ideal-theoretic approach to work problems and unification problems over finitely presented commutative algebras. In Jean-Pierre Jouannaud, editor, Rewriting Techniques and Applications, First International Conference, RTA-85, Dijon, France, May 20-22, 1985, Proceedings, volume 202 of Lecture Notes in Computer Science, pages 345-364. Springer, 1985. URL: https://doi.org/10.1007/3-540-15976-2_17.
  12. Abdelilah Kandri-Rody, Deepak Kapur, and Franz Winkler. Knuth-bendix procedure and buchberger algorithm: A synthesis. In Gaston H. Gonnet, editor, Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC '89, Portland, Oregon, USA, July 17-19, 1989, pages 55-67. ACM, 1989. URL: https://doi.org/10.1145/74540.74548.
  13. Deepak Kapur. Shostak’s congruence closure as completion. In Hubert Comon, editor, Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of Lecture Notes in Computer Science, pages 23-37. Springer, 1997. URL: https://doi.org/10.1007/3-540-62950-5_59.
  14. Deepak Kapur. Conditional congruence closure over uninterpreted and interpreted symbols. J. Syst. Sci. Complex., 32(1):317-355, 2019. URL: https://doi.org/10.1007/s11424-019-8377-8.
  15. Deepak Kapur. Weird gröbner bases: An application of associative-commutative congruence closure algorithm. Tech report under preparation, Department of Computer Science, University of New Mexico, May 2021. Google Scholar
  16. Deepak Kapur and Yongyang Cai. An algorithm for computing a gröbner basis of a polynomial ideal over a ring with zero divisors. Math. Comput. Sci., 2(4):601-634, 2009. URL: https://doi.org/10.1007/s11786-009-0072-z.
  17. Deepak Kapur, David R. Musser, and Paliath Narendran. Only prime superpositions need be considered in the knuth-bendix completion procedure. J. Symb. Comput., 6(1):19-36, 1988. URL: https://doi.org/10.1016/S0747-7171(88)80019-1.
  18. Deepak Kapur and Paliath Narendran. Double-exponential complexity of computing a complete set of ac-unifiers. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992, pages 11-21. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/LICS.1992.185515.
  19. Deepak Kapur and Hantao Zhang. An overview of rewrite rule laboratory (rrl). Computers and Mathematics Applications, 29:91-114, 1995. Google Scholar
  20. Donald Knuth and Peter Bendix. Simple word problems in universal algebras. In Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970. Google Scholar
  21. Claude Marché. On ground ac-completion. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 411-422. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_114.
  22. Claude Marché. Normalized rewriting: An alternative to rewriting modulo a set of equations. J. Symb. Comput., 21(3):253-288, 1996. URL: https://doi.org/10.1006/jsco.1996.0011.
  23. Ernst W. Mayr and Albert Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46:305-439, 1982. Google Scholar
  24. Paliath Narendran and Michaël Rusinowitch. Any gound associative-commutative theory has a finite canonical system. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 423-434. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_115.
  25. Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356-364, 1980. URL: https://doi.org/10.1145/322186.322198.
  26. Robert Nieuwenhuis and Albert Oliveras. Fast congruence closure and extensions. Inf. Comput., 205(4):557-580, 2007. URL: https://doi.org/10.1016/j.ic.2006.08.009.
  27. Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233-264, 1981. URL: https://doi.org/10.1145/322248.322251.
  28. Robert E. Shostak. An algorithm for reasoning about equality. Commun. ACM, 21(7):583-585, 1978. URL: https://doi.org/10.1145/359545.359570.
  29. Franz Winkler. Canonical forms in the finitely presented algebras. Ph.d. dissertation, U. of Paris 11, 1983. Google Scholar
  30. Franz Winkler. The Church-Rosser Property in Computer Algebra and Special Theorem Proving: An Investigation of Critical-Pair/Completion Algorithms. Ph.d. dissertation, University of Linz, 1984. Google Scholar
  31. Chee-Keng Yap. A new lower bound construction for commutative thue systems with aapplications. J. Symb. Comput., 12(1):1-28, 1991. URL: https://doi.org/10.1016/S0747-7171(08)80138-1.
  32. Hantao Zhang. Implementing contextual rewriting. In Michaël Rusinowitch and Jean-Luc Rémy, editors, Conditional Term Rewriting Systems, Third International Workshop, CTRS-92, Pont-à-Mousson, France, July 8-10, 1992, Proceedings, volume 656 of Lecture Notes in Computer Science, pages 363-377. Springer, 1992. URL: https://doi.org/10.1007/3-540-56393-8_28.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact