Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke:
Improving Dependency Pairs
In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), Almaty, Kazakhstan.
Lecture Notes in Artificial Intelligence 2850, pages 167-182, 2003. ©Springer-Verlag

The dependency pair approach is one of the most powerful techniques for termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by weakly monotonic well-founded orders. We improve the dependency pair approach by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs which simplify (innermost) termination proofs significantly. In order to fully automate the dependency pair approach, we show how transformation techniques and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples.

[ BibTeX | Paper (ps.gz) | Paper (pdf) | Paper on SpringerLink ]