Artículo
Formal verification of a generic framework to synthesize SAT-provers
Autor/es | Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2004 |
Fecha de depósito | 2019-05-10 |
Publicado en |
|
Resumen | We present in this paper an application of the ACL2 system to generate
and reason about propositional satis ability provers. For that purpose, we develop a
framework where we de ne a generic SAT-prover based on transformation ... We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability provers. For that purpose, we develop a framework where we de ne a generic SAT-prover based on transformation rules, and we formalize this generic framework in the ACL2 logic, carrying out a formal proof of its termination, soundness and completeness. This generic framework can be instantiated to obtain a number of veri ed and executable SAT-provers in ACL2, and this can be done in an automated way. Three instantiations of the generic framework are considered: semantic tableaux, sequent and Davis-Putnam-Logeman-Loveland methods. |
Identificador del proyecto | TIC2000-1368-C03-02 |
Cita | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2004). Formal verification of a generic framework to synthesize SAT-provers. Journal of Automated Reasoning, 32 (287) |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
2004-JAR.pdf | 397.9Kb | [PDF] | Ver/ | |