The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Dear Brad,

I just want to point out the SMTCoq ongoing work
<http://cs.au.dk/~chkeller/Recherche/smtcoq.html> aiming at verifying
SAT and SMT proof witnesses inside Coq. Basic tactics are written on top
of it. Experiments show that the possibly exponential proof witnesses do
not produce a blow up when checking them compared to finding them.

It includes CNF-conversion checking in the Tseitin style. It could
indeed be a good idea to provide a top-level tactic just doing this
conversion, independently from external SAT and SMT solvers.

Best,
Chantal KELLER.