The Derivational Complexity Induced by the Dependency Pair Method

We study the derivational complexity induced by the (basic) dependency pair method. Suppose the derivational complexity induced by a termination method is closed under elementary functions. We show that the derivational complexity induced by the dependency pair method based on this termination technique is the same as for the direct technique. Therefore, the derivational complexity induced by the dependency pair method based on lexicographic path orders or multiset path orders is multiple recursive or primitive recursive, respectively. Moreover for the dependency pair method based on Knuth-Bendix orders, we obtain that the derivational complexity function is majorised by the Ackermann function. These characterisations are essentially optimal.

• Type: Conference
• Year: 2009
• Where: RTA
• Authors: Georg Moser, Andreas Schnabl
• Keywords: Dependency Pair Method, Derivational Complexity, RTA 2009, Termination Method, Theoretical Computer Science