Termination of term rewriting using dependency pairs

We present techniques to prove termination and innermost termination of ter m rewriting systems automatically. In contrast to previous approaches, we d o not compare left- and right-hand sides of rewrite rules, but introduce th e notion of dependency pairs to compare left-hand sides with special subter ms of the right-hand sides. This results in a technique which allows to app ly existing methods for automated termination proofs to term rewriting syst ems where they failed up to now. In particular, there are numerous term rew riting systems where a direct termination proof with simplification orderin gs is not possible, but in combination with our technique, well-known simpl ification orderings (such as the recursive path ordering, polynomial orderi ngs, or the Knuth-Bendix ordering) can now be used to prove termination aut omatically. Unlike previous methods, our technique for proving innermost te rmination automatically can also be applied to prove innermost termination of term rewriting systems that are not terminating. Moreover, as innermost termination implies termination for certain classes of term rewriting syste ms, this technique can also be used for termination proofs of such systems. (C) 2000 Elsevier Science B.V. All rights reserved.