2005-03: Proving and Disproving Termination of Higher-Order Functions
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.
participants (1)
-
Volker Stolz