In this paper we study how to extend a collection of term orderings on disjoint signatures to a single one, caned 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 some new 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 new symbols.
CITATION STYLE
Rubio, A. (1995). Extension orderings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 944, pp. 511–522). Springer Verlag. https://doi.org/10.1007/3-540-60084-1_101
Mendeley helps you to discover research relevant for your work.