Formal Correctness of a Quadratic Unification Algorithm

Ruiz Reina, José Luis; Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José

doi:10.1007/s10817-006-9030-5

Artículo

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

Ficheros	Tamaño	Formato	Ver	Descripción
2006-jar.pdf	215.3Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Artículos (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional