The following technical report is available from http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp: Proving and Disproving Termination of Higher-Order Functions AIB 2005-03
The dependency pair technique is one of the most powerful methods for automated termination proofs of term rewrite systems (TRSs). We present two important extensions of this technique: First, we show how to prove termination of higher-order functions with dependency pairs. To this end, the dependency pair technique is extended to handle (untyped) applicative TRSs. Second, we introduce a method to prove non- termination in the dependency pair framework, while up to now dependency pairs were only used to verify termination. We implemented and evaluated our results in the automated termination prover AProVE.