Martín-Mateos, F. J.; Alonso, J. A.; Hidalgo, M. J.; Ruiz-Reina, J. L. Verification in ACL2 of a generic framework to synthesize SAT-provers. (English) Zbl 1278.68273 Leuschel, Michael (ed.), Logic based program synthesis and transformation. 12th international workshop, LOPSTR 2002, Madrid, Spain, September 17–20, 2002. Revised selected papers. Berlin: Springer (ISBN 3-540-40438-4/pbk). Lecture Notes in Computer Science 2664, 182-198 (2003). Summary: 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.For the entire collection see [Zbl 1045.68013]. Cited in 1 Document MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Software:ECCE; TOY; ACL2 PDFBibTeX XMLCite \textit{F. J. Martín-Mateos} et al., Lect. Notes Comput. Sci. 2664, 182--198 (2003; Zbl 1278.68273) Full Text: DOI