Mostrar el registro sencillo del ítem
dc.contributor.author | Lucas Alba, Salvador | es_ES |
dc.contributor.author | Gutiérrez Gil, Raúl | es_ES |
dc.date.accessioned | 2019-06-01T20:01:13Z | |
dc.date.available | 2019-06-01T20:01:13Z | |
dc.date.issued | 2018 | es_ES |
dc.identifier.issn | 0020-0190 | es_ES |
dc.identifier.uri | http://hdl.handle.net/10251/121414 | |
dc.description.abstract | [EN] Given a (Conditional) Rewrite System R and terms s and t, we consider the following problem: is there a substitution a instantiating the variables in s and t such that the reachability test sigma(s) -> *(R) sigma(t) succeeds? If such a substitution does not exist, we say that the problem is infeasible; otherwise, we call it feasible. Similarly, we can consider reducibility, involving a single rewriting step. In term rewriting, a number of important problems involve such infeasibility tests (e.g., confluence and termination analysis). We show how to recast infeasibility tests into the problem of finding a model of a set of (first-order) sentences representing the operational semantics of R together with some additional sentences representing the considered property which is formulated as an infeasibility test. (C) 2018 Elsevier B.V. All rights reserved. | es_ES |
dc.description.sponsorship | Partially supported by the EU (FEDER) which is co-funding the project TIN2015-69175-C4-1-R, Spanish MINECO project TIN2015-69175-C4-1-R and Generalitat Valenciana (GV) project PROMETEOII/2015/013. | es_ES |
dc.language | Inglés | es_ES |
dc.publisher | Elsevier | es_ES |
dc.relation.ispartof | Information Processing Letters | es_ES |
dc.rights | Reconocimiento - No comercial - Sin obra derivada (by-nc-nd) | es_ES |
dc.subject | Conditional rewriting | es_ES |
dc.subject | Confluence | es_ES |
dc.subject | Dependency graph | es_ES |
dc.subject | Operational termination | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Use of logical models for proving infeasibility in term rewriting | es_ES |
dc.type | Artículo | es_ES |
dc.identifier.doi | 10.1016/j.ipl.2018.04.002 | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ | es_ES |
dc.rights.accessRights | Abierto | es_ES |
dc.contributor.affiliation | Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació | es_ES |
dc.description.bibliographicCitation | Lucas Alba, S.; Gutiérrez Gil, R. (2018). Use of logical models for proving infeasibility in term rewriting. Information Processing Letters. 136:90-95. https://doi.org/10.1016/j.ipl.2018.04.002 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.publisherversion | http://doi.org/10.1016/j.ipl.2018.04.002 | es_ES |
dc.description.upvformatpinicio | 90 | es_ES |
dc.description.upvformatpfin | 95 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.description.volume | 136 | es_ES |
dc.relation.pasarela | S\364101 | es_ES |
dc.contributor.funder | Generalitat Valenciana | es_ES |
dc.contributor.funder | Ministerio de Economía y Empresa | es_ES |