Approximating dependency graphs using tree automata techniques. (English) Zbl 0988.68162
Goré, Rajeev (ed.) et al., Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2083, 593-610 (2001).
Summary: The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved by using tree automata techniques to obtain better approximations of the dependency graph. This graph determines the ordering constraints that need to be solved in order to conclude termination. We further show that by using our approximations the dependency pair method provides a decision procedure for termination of right-ground rewrite systems.
For the entire collection see [Zbl 0968.00052].
For the entire collection see [Zbl 0968.00052].
MSC:
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
68Q42 | Grammars and rewriting systems |
68Q45 | Formal languages and automata |