2026-07-22T12:15:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3120 2024-03-06T10:33:51Z ddc:004 open_access

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity Moser, Georg Schnabl, Andreas Complexity DP Framework Multiple Recursive Functions We study the complexity of rewrite systems shown terminating via the dependency pair framework using processors for reduction pairs, dependency graphs, or the subterm criterion. The complexity of such systems is bounded by a multiple recursive function, provided the complexity induced by the employed base techniques is at most multiple recursive. Moreover this upper bound is tight. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Georg Moser and Andreas Schnabl 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.235 urn:nbn:de:0030-drops-31208 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.235 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode