The following technical report is available from http://aib.informatik.rwth-aachen.de/:

Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke

Mechanizing Dependency Pairs 2003-08

Abstract: The dependency pair approach is a powerful technique for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by 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 mechanize the approach, we show how transformations 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.