Georg Moser ; Andreas Schnabl - The Derivational Complexity Induced by the Dependency Pair Method

lmcs:805 - Logical Methods in Computer Science, July 13, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:1)2011
The Derivational Complexity Induced by the Dependency Pair MethodArticle

Authors: Georg Moser ; Andreas Schnabl

    We study the derivational complexity induced by the dependency pair method, enhanced with standard refinements. We obtain upper bounds on the derivational complexity induced by the dependency pair method in terms of the derivational complexity of the base techniques employed. In particular we show that the derivational complexity induced by the dependency pair method based on some direct technique, possibly refined by argument filtering, the usable rules criterion, or dependency graphs, is primitive recursive in the derivational complexity induced by the direct method. This implies that the derivational complexity induced by a standard application of the dependency pair method based on traditional termination orders like KBO, LPO, and MPO is exactly the same as if those orders were applied as the only termination technique.


    Volume: Volume 7, Issue 3
    Published on: July 13, 2011
    Imported on: October 11, 2010
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Artificial Intelligence,Computer Science - Computational Complexity,Computer Science - Programming Languages,F.4.1, F.2.2, D.2.4, D.2.8
    Funding:
      Source : OpenAIRE Graph
    • Derivational Complexity Analysis; Funder: Austrian Science Fund (FWF); Code: P 20133

    6 Documents citing this article

    Consultation statistics

    This page has been seen 930 times.
    This article's PDF has been downloaded 291 times.