Ruiz Reina, José LuisAlonso Jiménez, José AntonioHidalgo Doblado, María JoséMartín Mateos, Francisco Jesús2021-03-162021-03-162002Ruiz 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.https://hdl.handle.net/11441/106121We 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.application/pdf7engAttribution-NonCommercial-NoDerivatives 4.0 Internacionalhttp://creativecommons.org/licenses/by-nc-nd/4.0/info:eu-repo/semantics/conferenceObjectinfo:eu-repo/semantics/openAccess