Rewrite Closure for Ground and Cancellative AC Theories

  • Ashish Tiwari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


Given a binary relation Open image in new window on the set of ground terms over some signature, we define an abstract rewrite closure for Open image in new window . An abstract rewrite closure can be interpreted as a specialized ground tree transducer (pair of bottom-up tree automata) and can be used to efficiently decide the reachability relation Open image in new window . It is constructed using a completion like procedure. Correctness is established using proof ordering techniques. The procedure is extended, in a modular way, to deal with signatures containing cancellative associative commutative function symbols.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    L. Bachmair. Canonical Equational Proofs. Birkhäuser, Boston, 1991.zbMATHGoogle Scholar
  2. 2.
    L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2 & 3):173–201, October 1989.CrossRefMathSciNetzbMATHGoogle Scholar
  3. 3.
    L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41:236–276, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of binary relations. Technical Report MPI-I-95-2-009, 1995.Google Scholar
  5. 5.
    L. Bachmair, I.V. Ramakrishnan, A. Tiwari, and L. Vigneron. Congruence closure modulo associativity and commutativity. In Frontiers of Combining Systems, 3rd Intl Workshop FroCoS 2000, pages 245–259. Springer, 2000. LNAI 1794.Google Scholar
  6. 6.
    L. Bachmair and A. Tiwari. Abstract congruence closure and specializations. In D. McAllester, editor, CADE, pages 64–78. Springer, 2000. LNAI 1831. Full version to appear in J. of Automated Reasoning,
  7. 7.
    T. Becker and V. Weispfenning. Gröbner bases: a computational approach to commutative algebra. Springer-Verlag, Berlin, 1993.zbMATHGoogle Scholar
  8. 8.
    H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available at:, 1997.
  9. 9.
    M. Dauchet, T. Heuillard, P. Lescanne, and S. Tison. Decidability of the confluence of ground termrewriting systems. In Proc IEEE Symposium on Logic in Computer Science, LICS, pages 353–359. IEEE Computer Society Press, 1987.Google Scholar
  10. 10.
    C. Kirchner, editor. Rewriting Techniques and Applications, RTA-93, Montreal, Canada, 1993. Springer-Verlag. LNCS 690.Google Scholar
  11. 11.
    A. Levy and J. Agusti. Bi-rewriting, a termrewriting technique for monotone order relations. In Kirchner, pages 17–31. LNCS 690.Google Scholar
  12. 12.
    E. W. Mayr. Persistence of vector replacement systems is decidable. Acta Informatica 15, pages 309–318, 1981. NewsletterInfo: 8.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    D. A. Plaisted. Polynomial time termination and constraint satisfaction tests. In Kirchner [10], pages 405–420. LNCS 690.Google Scholar
  14. 14.
    S. Rao Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14th annual ACM symposium on theory of computing, pages 267–281, May 1982.Google Scholar
  15. 15.
    A. Rubio and R. Nieuwenhuis. A precedence-based total AC-compatible ordering. In Kirchner [10], pages 374–388. LNCS 690.Google Scholar
  16. 16.
    A. Tiwari. Rewrite closure for ground and cancellative AC theories. Available:, 2001. Full version of this paper.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Ashish Tiwari
    • 1
  1. 1.SRI InternationalUSA

Personalised recommendations