Beyond Dependency Graphs

The dependency pair framework is a powerful technique for proving termination of rewrite systems. One of the most frequently used methods within the dependency pair framework is the dependency graph processor. In this note we improve this processor by incorporating right-hand sides of forward closures. In combination with tree automata completion we obtain an efficient processor which can be used instead of the dependency graph approximations that are in common use in termination provers.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Martin Korp, Aart Middeldorp
• Keywords: Automated Reasoning, CADE 2009, Dependency Graph Approximations, Dependency Graph Processor, Dependency Pair Framework