The Coq mailing list

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

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
>>
>>
>