Abstract

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.

BibTeX

@article{GMAS-LMCS11,
  author  = "Georg Moser and Andreas Schnabl",
  title   = "The Derivational Complexity Induced by the Dependency Pair
             Method",
  journal = "Logical Methods in Computer Science",
  volume  = 7,
  number  = "3:1",
  pages   = "1 -- 38",
  year    = 2011
}