Repositorio de producción científica de la Universidad de Sevilla

Formal verification of a generic framework to synthesize SAT-provers

 

Advanced Search
 
Opened Access Formal verification of a generic framework to synthesize SAT-provers
Cites

Show item statistics
Icon
Export to
Author: 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
Date: 2004
Published in: Journal of Automated Reasoning, 32 (287)
Document type: Article
Abstract: 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.
Cite: 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)
Size: 397.9Kb
Format: PDF

URI: https://hdl.handle.net/11441/86269

DOI: 10.1007/BF03177742

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)