Approximating Dependency Graphs Using Tree Automata Techniques

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.

• Type: Conference
• Year: 2001
• Where: CADE
• Authors: Aart Middeldorp
• Keywords: CADE 2001, Dependency Pair Method, Rewrite Systems, Term Rewrite Systems