Rewrite Closure for Ground and Cancellative AC Theories
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.
- 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.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.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, http://www.csl.sri.com/users/tiwari/.
- 8.H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available at: http://www.grappa.univ-lille3.fr/tata, 1997.
- 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.C. Kirchner, editor. Rewriting Techniques and Applications, RTA-93, Montreal, Canada, 1993. Springer-Verlag. LNCS 690.Google Scholar
- 11.A. Levy and J. Agusti. Bi-rewriting, a termrewriting technique for monotone order relations. In Kirchner, pages 17–31. LNCS 690.Google Scholar
- 13.D. A. Plaisted. Polynomial time termination and constraint satisfaction tests. In Kirchner , pages 405–420. LNCS 690.Google Scholar
- 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.A. Rubio and R. Nieuwenhuis. A precedence-based total AC-compatible ordering. In Kirchner , pages 374–388. LNCS 690.Google Scholar
- 16.A. Tiwari. Rewrite closure for ground and cancellative AC theories. Available: http://www.csl.sri.com/users/tiwari/fsttcs01.html, 2001. Full version of this paper.