Por favor, use este identificador para citar o enlazar a este item:
http://hdl.handle.net/10261/160137
COMPARTIR / EXPORTAR:
SHARE CORE BASE | |
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE | |
Título: | Bi-Rewrite Systems |
Autor: | Levy, Jordi CSIC ORCID ; Agustí-Cullel, Jaume CSIC | Fecha de publicación: | 1996 | Editor: | Elsevier | Citación: | Journal of Symbolic Computation 22: 279- 314 (1996) | Resumen: | In this article we propose an extension of term rewriting techniques to automate the deduction in monotone pre-order theories. To prove an inclusionabfrom a given setIof them, we generate fromI, using a completion procedure, abi-rewrite system, that is, a pair of rewrite relations and , and seek a common termcsuch thatacandbc. Each component of the bi-rewrite system and is allowed to be a subset of the corresponding inclusion relation or defined by the theory ofI. In order to assure the decidability and completeness of such proof procedure we study the termination and commutation of and . The proof of the commutation property is based on a critical pair lemma, using anextendeddefinition of critical pair. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. Although we center our attention on the completion process á la Knuth–Bendix, the same notion of extended critical pairs is suitable to be applied to the so-called unfailing completion procedures. The completion process is illustrated by means of an example corresponding to the theory of the union operator. We show that confluence ofextendedcritical pairs may be ensured addingrule schemes. Such rule schemes contain variables denoting schemes of expressions, instead of expressions. We propose the use of thelinear second-order typedλ-calculustocodifythese expression schemes. Although the general second-order unification problem is only semi-decidable, the second-order unification problems we need to solve during the completion process are decidable. | URI: | http://hdl.handle.net/10261/160137 | DOI: | 10.1006/jsco.1996.0053 | Identificadores: | doi: 10.1006/jsco.1996.0053 issn: 0747-7171 |
Aparece en las colecciones: | (IIIA) Artículos |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
accesoRestringido.pdf | 15,38 kB | Adobe PDF | Visualizar/Abrir |
CORE Recommender
SCOPUSTM
Citations
21
checked on 11-abr-2024
WEB OF SCIENCETM
Citations
15
checked on 25-feb-2024
Page view(s)
196
checked on 19-abr-2024
Download(s)
33
checked on 19-abr-2024
Google ScholarTM
Check
Altmetric
Altmetric
NOTA: Los ítems de Digital.CSIC están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.