Verifying SAT and SMT in Coq for a fully automated decision procedure

Autor: Armand, Mickaël, Faure, Germain, Grégoire, Benjamin, Keller, Chantal, Théry, Laurent, Wener, Benjamin

Publikováno v: PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland

International audience; Enjoying the power of SAT and SMT solvers in the Coq proof as- sistant without compromising soundness requires more than a yes/no answer from them. SAT and SMT solvers should also return a proof witness that can be checked by

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::72e05b6b9451ee6b30e1fef987e3abb4
https://hal.inria.fr/inria-00614041/document