The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

This seems to be a FAQ. Any volunteers to put it into cocorico?

On Fri, May 15, 2015 at 9:37 AM, Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

Stéphane Lescuyer implemented a SMT-solver (a subset of Alt-Ergo)
directly in Coq:
  A reflexive formalization of a SAT solver in Coq.
  http://www.lri.fr/~conchon/publis/lescuyer-conchon-tphols08.pdf
  Stéphane Lescuyer and Sylvain Conchon. TPHOLs, 2008

  Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
  http://tel.archives-ouvertes.fr/docs/00/71/36/68/PDF/VA2_LESCUYER_STEPHANE_04012011.pdf
  Stéphane Lescuyer. PhD thesis, 2011

I think however that the resulting software has not been maintained since.

To my knowledge the state-of-the-art work on integration of SAT/SMT
solvers with Coq is the work of Chantal Keller:
  http://prosecco.gforge.inria.fr/personal/ckeller/recherche-en.html
(which includes your citation [1])
and in particular the actively maintained SMTCoq software :
  https://github.com/smtcoq/smtcoq
which accepts proof certificates from zChaff and VeriT.

On Fri, May 15, 2015 at 8:57 AM, stvienna wiener <stvienna AT gmail.com> wrote:
> Hi all,
>
>
> Where can I start looking about the state of the art of automation in Coq? I
> have read that there is ongoing work on SMT/SAT integration, as well as
> automation support for resolution and rewriting proofs.
>
>
> Are there any current papers I should look at?
>
>
> By “Coq automation”, I mean automation regarding resolution, rewriting and
> SAT/SMT solver integration. I am less interested in the basic automation
> tools (auto, trivial or omega).
>
>
> So far I have looked at the Coq workshop, ITP and the issues Journal of
> Automated reasoning for the last six years. I am aware that my question is
> rather broad and I still have some literature research to do. However, I
> would be glad if I get pointers into the right direction.
>
>
> Best regards from Vienna,
>
> Steve
>
>
> PS: these are the papers I found so far:
>
>
> [1] Armand, Michaël, et al. "A modular integration of SAT/SMT solvers to Coq
> through proof witnesses." Certified Programs and Proofs. Springer Berlin
> Heidelberg, 2011. 135-150.
>
>
> [2] Blanqui, Frédéric, and Adam Koprowski. "CoLoR: a Coq library on
> well-founded rewrite relations and its application to the automated
> verification of termination certificates." Mathematical Structures in
> Computer Science 21.04 (2011): 827-859.
>
>
> [3] Strub, Pierre-Yves. "Coq modulo theory." Computer Science Logic.
> Springer Berlin Heidelberg, 2010.
>
>
> [4] Boldo, Sylvie, Jean-Christophe Filliâtre, and Guillaume Melquiond.
> "Combining Coq and Gappa for certifying floating-point programs."
> Intelligent Computer Mathematics. Springer Berlin Heidelberg, 2009. 59-74.
>
>
> [5] Bezem, Marc, Dimitri Hendriks, and Hans De Nivelle. "Automated proof
> construction in type theory using resolution." Journal of Automated
> Reasoning 29.3 (2002): 253-275.