Dependency Graphs, Relative Rule Removal, and Derivational Complexity


This talk deals with dependency graphs, one of the fundamental refinements
of the dependency pair method, which is a very important technique in
automatic termination proving of term rewrite systems. We analyse upper
bounds on the derivational complexity of rewrite systems whose termination
is shown by this technique. We consider both the setting where each
strongly connected component of the dependency graph is handled in a single
step by a basic termination proof technique, and the setting where the
rules in the strongly connected components are removed successively by the
reduction pair processor of the dependency pair framework.