The following technical report is available from http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp and Stephan Falke Improving Dependency Pairs 2003-04
Abstract: 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.
Regards, Volker