Ponencia
A Theory About First-Order Terms in ACL2
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 describe the development in ACL2 of a library of results about first-order
terms. In particular, we present the formalization of some of the main properties of the
complete lattice of first-order terms with respect ... We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the formalization of some of the main properties of the complete lattice of first-order terms with respect to the subsumption relation. As a byproduct, verified executable implementations are obtained for some basic operations on firstorder terms, including matching, renaming, unification and anti-unification. This work can be seen as a basis for further studies about the formal properties of automated reasoning and symbolic computation systems. |
Agencias financiadoras | Ministerio de Ciencia Y Tecnología (MCYT). España |
Identificador del proyecto | TIC2000-1368-CO3-02 |
Cita | Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2002). A Theory About First-Order Terms in ACL2. En ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications Grenoble, France: University of Texas. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
A theory about first-order terms ... | 244.9Kb | [PDF] | Ver/ | |