The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

While this seems interesting as an academic pursuit, I wonder if it's at all practical.  Are there any SAT solvers which don't also output certificates?

Kris

On Wed, Dec 4, 2013 at 4:53 PM, Bradford Larsen <brad.larsen AT gmail.com> wrote:

Is there any work proving the correctness of the Tseitin transformation or other propositional logic transformations in Coq?

More generally, I'm interested in seeing what existing work has been done on formalizing the algorithms used in SAT/SMT solvers.

Thanks,

Brad Larsen