2007/01/01 by René Thiemann, Thiemann, René, Jürgen Giesl +3
Computer Science · #Advanced Database Systems and Queries #Decision Procedures #Dependency Pairs #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Non-Termination #Term Rewriting
paper · doi:10.4230/dagsemproc.07401.3
openalex publication_date 2007/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.