Presentation
Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers
Author/s | Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Ruiz Reina, José Luis |
Department | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Publication Date | 2002 |
Deposit Date | 2019-05-16 |
Published in |
|
ISBN/ISSN | 978-3-540-40438-5 0302-9743 |
Abstract | We present in this paper an application of the ACL2 system
to reason about propositional satisfiability provers. For that purpose,
we present a framework where we define a generic transformation based
SAT–prover, and ... We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that purpose, we present a framework where we define a generic transformation based SAT–prover, and we show how this generic framework can be formalized in the ACL2 logic, making a formal proof of its termination, soundness and completeness. This generic framework can be instantiated to obtain a number of verified and executable SAT–provers in ACL2, and this can be done in an automatized way. Three case studies are considered: semantic tableaux, sequent and Davis–Putnam methods. |
Project ID. | TIC2000-1368-C03-02 |
Citation | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2002). Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers. En LOPSTR 2002: 12th International Workshop on on Logic-Based Program Synthesis and Transformation (182-198), Madrid, España: Springer. |
Files | Size | Format | View | Description |
---|---|---|---|---|
Verification in ACL2 of a Generic ... | 204.4Kb | [PDF] | View/ | |