| Abstract: | We present in this paper an application of the ACL2 system to generate and reason about propositional satisfiability provers.
For that purpose, we develop a framework in which we define a generic S AT-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 verified and executable SAT-provers in ACL2, and this instantiation
can be done in an automated way. Three instantiations of the generic framework are considered: semantic tableaux, sequent
calculus, and Davis-Putnam-Logeman-Loveland methods. |
