Decision Procedures for Loop Detection

Abstract. The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems. We first show that dependency pairs are also suitable for disproving termination: loops can be detected more easily. In a second step we analyze how to disprove innermost termination. Here, we present a novel procedure to decide whether a given loop is an innermost loop. All results have been implemented in the termination prover AProVE. Keywords. Non-Termination, Decision Procedures, Term Rewriting, Dependency Pairs

• Type: Conference
• Year: 2007
• Where: DAGSTUHL
• Authors: René Thiemann, Jürgen Giesl, Peter Schneider-Kamp
• Keywords: DAGSTUHL 2007, Dependency Pair Technique, Dependency Pairs, Software Engineering, Termination Proofs