dc.creator | Ruiz Reina, José Luis | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.date.accessioned | 2019-05-09T08:06:06Z | |
dc.date.available | 2019-05-09T08:06:06Z | |
dc.date.issued | 2006 | |
dc.identifier.citation | Ruiz Reina, J.L., Martín Mateos, F.J., Alonso Jiménez, J.A. y Hidalgo Doblado, M.J. (2006). Formal Correctness of a Quadratic Unification Algorithm. Journal of Automated Reasoning, 37 (1-2), 67-92. | |
dc.identifier.issn | 0168-7433 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86262 | |
dc.description.abstract | We present a case study using ACL2 [5] to verify a non-trivial algorithm
that uses efficient data structures. The algorithm receives as input two first-order
terms and it returns a most general unifier of these terms if they are unifiable, failure
otherwise. The verified implementation stores terms as directed acyclic graphs by
means of a pointer structure. Its time complexity is O(n2) and its space complexity
is O(n), and it can be executed in ACL2 at a speed comparable to a similar C
implementation. We report the main issues encountered to achieve this formally
verified implementation. | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | Journal of Automated Reasoning, 37 (1-2), 67-92. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Formal Correctness of a Quadratic Unification Algorithm | 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 Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.publisherversion | https://link.springer.com/article/10.1007/s10817-006-9030-5 | es |
dc.identifier.doi | 10.1007/s10817-006-9030-5 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 31 | es |
dc.journaltitle | Journal of Automated Reasoning | es |
dc.publication.volumen | 37 | es |
dc.publication.issue | 1-2 | es |
dc.publication.initialPage | 67 | es |
dc.publication.endPage | 92 | es |
dc.identifier.sisius | 6674508 | es |