The Coq mailing list

[Evelyne Contejean <Evelyne.Contejean AT lri.fr>]

There is also the "ergo" tactic, due to Stéphane Lescuyer, as a part of 
his thesis when he was a PhD student of mine.

www.lix.polytechnique.fr/coq/pylons/.../Ergo/v8.3

This tactic is based on the SMT solver Alt-Ergo developed by me and 
Sylvain Conchon.

Regards,

Évelyne Contejean


On 04/28/2015 05:38 PM, Chantal Keller wrote:
> Thanks Beta for pointing this out. SMTCoq is now available via Github:
> <https://github.com/smtcoq/smtcoq>.
>
> However, it does not provide support for the kind of problems you are
> asking. One of its objectives is to automatically solve goals that can
> be handled by SMT solvers, but it is not linked so deeply with Coq's
> type inference mechanism. That could indeed be of interest.
>
> Best,
> Chantal.
>
>
>
> Le 28/04/2015 17:26, Beta Ziliani a écrit :
> > I think the work SMTCoq might be of help:
> > http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html
> >
> >
> > On Tue, Apr 28, 2015 at 12:23 PM, Jonathan Leivent 
> > <jonikelee AT gmail.com>
> > wrote:
> >
> > > Does anyone know of any work linking an SMT solver to Coq?
> > >
> > > In particular, I'm wondering if it would be better to view multiple goals
> > > in Coq that are inter-dependent through shared evars as a satisfiability
> > > problem for the evars, or perhaps as some hybrid of satisfiability and
> > > proving.
> > >
> > > Unfortunately, I don't know much about SMT, or related fields like
> > > constraint-based programming - just enough to think (hope?) that these
> > > might offer something useful to Coq with respect to solving
> > > evar-interdependent goals - something to supplement Coq's own backtracking
> > > proof search automation.
> > >
> > > -- Jonathan