DagSemProc.07401.3.pdf
- Filesize: 309 kB
- 17 pages
Document
Decision Procedures for Loop Detection
Authors
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 7401
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2007-11-29
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
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)
0PDF Downloads