dc.creator | Galán Morillo, Francisco José | es |
dc.creator | Cañete Valdeón, José Miguel | es |
dc.date.accessioned | 2020-06-18T08:57:18Z | |
dc.date.available | 2020-06-18T08:57:18Z | |
dc.date.issued | 2016 | |
dc.identifier.citation | Galán Morillo, F.J. y Cañete Valdeón, J.M. (2016). Synthesis of positive logic programs for checking a class of definitions with infinite quantification. Information and Computation, 249 (August 2016), 205-236. | |
dc.identifier.issn | 0890-5401 | es |
dc.identifier.uri | https://hdl.handle.net/11441/97976 | |
dc.description.abstract | We describe a method based on unfold/fold transformations that synthesizes positive logicprograms P(r)with the purpose of checking mechanically definitions of the form D(r) =∀X(r(X) ⇔QYR(X, Y))where ris the relation defined by the formula QYR(X, Y), Xis a set of variables to be instantiated at runtime by ground terms, QYis a set of quantifiedvariables on infinite domains (Qis the quantifier) and R(X, Y)a quantifier-free formulain the language of a first-order logic theory. This work constitutes a first step towards theconstruction of a new type of assertion checkers with the ability of handling restrictedforms of infinite quantification. | es |
dc.format | application/pdf | es |
dc.format.extent | 32 | es |
dc.language.iso | eng | es |
dc.publisher | Elsevier | es |
dc.relation.ispartof | Information and Computation, 249 (August 2016), 205-236. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Program assertion | es |
dc.subject | Logic program | es |
dc.subject | Program synthesis | es |
dc.subject | Unfold/fold transformation | es |
dc.title | Synthesis of positive logic programs for checking a class of definitions with infinite quantification | es |
dc.type | info:eu-repo/semantics/article | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos | es |
dc.relation.publisherversion | https://www.sciencedirect.com/science/article/abs/pii/S089054011630030X | es |
dc.identifier.doi | 10.1016/j.ic.2016.06.014 | es |
dc.journaltitle | Information and Computation | es |
dc.publication.volumen | 249 | es |
dc.publication.issue | August 2016 | es |
dc.publication.initialPage | 205 | es |
dc.publication.endPage | 236 | es |
dc.identifier.sisius | 21716712 | es |