Decision Procedures for Loop Detection

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



PDF
Thumbnail PDF

File

DagSemProc.07401.3.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)
https://doi.org/10.4230/DagSemProc.07401.3

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

Metrics

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