Extension orderings
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/96909
Tipus de documentReport de recerca
Data publicació1995-10
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
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.
CitacióRubio, A. "Extension orderings". 1995.
Forma partLSI-95-5-R
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
1400191309.pdf | 1,529Mb | Visualitza/Obre |