2026-07-20T05:27:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:509 2024-03-06T11:06:33Z ddc:004 open_access

Proving and Disproving Termination in the Dependency Pair Framework Giesl, Jürgen Thiemann, René Schneider-Kamp, Peter Termination non-termination term rewriting dependency pairs The dependency pair framework is a new general concept to integrate arbitrary techniques for termination analysis of term rewriting. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. Moreover, this framework facilitates the development of new methods for termination analysis. Traditionally, the research on termination focused on methods which prove termination and there were hardly any approaches for disproving termination. We show that with the dependency pair framework, one can combine the search for a proof and for a disproof of termination. In this way, we obtain the first powerful method which can also verify non-termination of term rewrite systems. We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving termination of term rewriting. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jürgen Giesl and René Thiemann and Peter Schneider-Kamp 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.05431.6 urn:nbn:de:0030-drops-5091 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.6 eng https://creativecommons.org/licenses/by/4.0/legalcode