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

lmcs:805 - Logical Methods in Computer Science, July 13, 2011, Volume 7, Issue 3
The Derivational Complexity Induced by the Dependency Pair Method

Authors: Moser, Georg and Schnabl, Andreas

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.


Source : oai:arXiv.org:0904.0570
DOI : 10.2168/LMCS-7(3:1)2011
Volume: Volume 7, Issue 3
Published on: July 13, 2011
Submitted 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


Share

Consultation statistics

This page has been seen 47 times.
This article's PDF has been downloaded 13 times.