Ponencia
Progress Report: Term Dags Using Stobjs
Autor/es | Ruiz Reina, José Luis
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Martín Mateos, Francisco Jesús |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2002 |
Fecha de depósito | 2021-03-16 |
Publicado en |
|
Resumen | We explore in this paper the use of efficient data structures to implement operations
on first-order terms, that can be formally verified. Specifically, we present the status
of our work on defining and verifying a ... We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be formally verified. Specifically, we present the status of our work on defining and verifying 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 representing the unification problem. |
Agencias financiadoras | Ministerio de Ciencia Y Tecnología (MCYT). España |
Identificador del proyecto | TIC2000–1368–C03–02 |
Cita | Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2002). Progress Report: Term Dags Using Stobjs. En ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications Grenoble, France: University of Texas. |