Extension orderings

Abstract

In this paper we study how to extend a collection of term orderings on disjoint signatures to a single one, called an extension ordering, which preserves (part of) their properties. Apart of its own interest, e.g. in automated deduction, extension orderings turn out to be a new method to obtain simple and constructive proofs for modularity of termination of TRS. Three different schemes to define extension orderings are given. The first one to deal with reduction orderings, the second one to extend simplification orderings and the last one for total reduction orderings. This provides simpler and more constructive proofs for some known modularity results for (simple and total) termination of rewriting as well as the first -- to our knowledge -- results for rewriting modulo equational theories. Finally, our technique is applied to extend an ordering on a given signature to a new one on the signature enlarged with some new symbols. Apart of its own iterest these extension orderings can sometimes be used to prove termination of hierarchical unions of TRS.