Pushing the Frontiers of Combining Rewrite Systems Farther Outwards.
Jürgen Giesl, Enno Ohlebusch · 1998
It is well known that simple termination is modular for certain kinds of combinations of term rewriting systems (TRSs). This result is of practical relevance because most techniques for (automated) termination proofs use simplification orderings, so they show in fact simple termination. On the other hand, in practice many systems are non-simply terminating. In order to cope with such systems, Arts and Giesl developed the dependency pair approach. By using (quasi-)simplification orderings in combination with dependency pairs, it is possible to prove termination of non-simply terminating systems automatically. It is natural to ask whether modularity of simple termination can be extended to the class of those systems which can be handled by this technique. In this paper we show that this is indeed the case. In this way, the class of TRSs for which termination can be proved in a modular way is extended significantly. 1 Introduction Modularity is a well-known paradigm in computer science. ...