Repositorio de producción científica de la Universidad de Sevilla

Formal Correctness of a Quadratic Unification Algorithm

 

Advanced Search
 
Opened Access Formal Correctness of a Quadratic Unification Algorithm
Cites

Show item statistics
Icon
Export to
Author: Ruiz Reina, José Luis
Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio
Hidalgo Doblado, María José
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2006
Published in: Journal of Automated Reasoning, 37 (1-2), 67-92.
Document type: Article
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.
Cite: 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.
Size: 215.3Kb
Format: PDF

URI: https://hdl.handle.net/11441/86262

DOI: 10.1007/s10817-006-9030-5

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)