×

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].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

ECCE; TOY; ACL2
PDFBibTeX XMLCite
Full Text: DOI