Formal verification of a generic framework to synthesize SAT-provers
| Autor: | José-Luis Ruiz-Reina, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Antonio Alonso |
|---|---|
| Přispěvatelé: | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial, Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento |
| Rok vydání: | 2004 |
| Předmět: |
Soundness
Programming language Sequent calculus ACL2 computer.file_format computer.software_genre Formal proof Satisfiability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Artificial Intelligence TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Completeness (logic) Executable Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION computer Formal verification Software computer.programming_language Mathematics |
| Zdroj: | idUS. Depósito de Investigación de la Universidad de Sevilla instname |
| ISSN: | 1573-0670 0168-7433 |
| Popis: | 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. Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink