Sciweavers

Share
DAGSTUHL
2007

Decision Procedures for Loop Detection

8 years 11 months ago
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
René Thiemann, Jürgen Giesl, Peter Sch
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Where DAGSTUHL
Authors René Thiemann, Jürgen Giesl, Peter Schneider-Kamp
Comments (0)
books