Artículo
Formal Correctness of a Quadratic Unification Algorithm
Autor/es | Ruiz Reina, José Luis
Martín Mateos, Francisco Jesús Alonso Jiménez, José Antonio Hidalgo Doblado, María José |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2006 |
Fecha de depósito | 2019-05-09 |
Publicado en |
|
Resumen | 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 ... 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. |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
2006-jar.pdf | 215.3Kb | [PDF] | Ver/ | |