Decision Procedures for Loop Detection

Authors René Thiemann, Jürgen Giesl, Peter Schneider-Kamp

Thumbnail PDF


  • Filesize: 309 kB
  • 17 pages

Document Identifiers

Author Details

René Thiemann
Jürgen Giesl
Peter Schneider-Kamp

Cite AsGet BibTex

René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp. Decision Procedures for Loop Detection. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


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.
  • Non-Termination
  • Decision Procedures
  • Term Rewriting
  • Dependency Pairs


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads