|
Abstract : |
Abstract. The framework of dependency pairs allows automated termination and innermost termination proofs for many TRSs where such proofs were not possible before. In this paper we present a refinement of this framework in order to prove termination in a modular way. Our modularity results significantly increase the class of term rewriting systems where termination resp. innermost termination can be proved automatically. Moreover, the modular approach to dependency pairs yields new modularity criteria which extend previous results in this area considerably. In particular, existing results for modularity of innermost termination can easily be obtained as direct consequences of our new criteria. 1, |
