Formal verification of a syntactic unification algorithm using dags

CLG, CCIA, University of Seville

Warning: This work is now obsolete. The current version of this work, with the verification of a quadratic unification algorithm is available at the web page of the ACL2 workshop 2004, including a paper, the supporting materials and slides of the presentation.

We present the definition and formal verification in ACL2 of a unification algorithm acting on terms represented as directed acyclic graphs (dags). This implementation is done using single-threaded objects (stobjs) to store a dag representation of first-order terms.

ACL2 books used in this development:

Dpto. de Ciencias de la Computación e Inteligencia Artificial
Escuela Técnica Superior de Ingeniería Informática
Universidad de Sevilla

Fomal verification in ACL2 of a dag based unification algorithm