Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
verfasst von : Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
Erschienen in: Certified Programs and Proofs
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a way to enjoy the power of SAT and SMT provers in
Coq
without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in
Coq
. It is conceived in a modular way, in order to tame the proofs’ complexity and to be extendable. It can currently check witnesses from the SAT solver
ZChaff
and from the SMT solver
veriT
. Experiments highlight the efficiency of this checker. On top of it, new reflexive
Coq
tactics have been built that can decide a subset of
Coq
’s logic by calling external provers and carefully checking their answers.