2026-07-22T21:48:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2422 2024-03-06T11:09:01Z ddc:004 open_access

Inductive Theorem Proving meets Dependency Pairs Swiderski, Stephan Parting, Michael Giesl, Jürgen Fuhs, Carsten Schneider-Kamp, Peter Termination Term Rewriting Dependency Pairs Inductive Theorem Proving Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stephan Swiderski and Michael Parting and Jürgen Giesl and Carsten Fuhs and Peter Schneider-Kamp 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.09411.4 urn:nbn:de:0030-drops-24220 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.4 eng https://creativecommons.org/licenses/by/4.0/legalcode