The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

I'm not very familiar with the field but I would also mention Stéphane
Lescuyer's 2011 PhD thesis, "Formalizing and Implementing a Reflexive
Tactic for Automated Deduction in Coq", which daringly implemented a
core SMT solver (a kernel of Alt-Ergo) directly in Coq. I'm not sure
if/where the resulting development is maintained.

On Wed, Apr 3, 2013 at 2:13 PM, Chantal Keller 
<Chantal.Keller AT inria.fr>
 wrote:
> Thanks Arnaud for pointing this out. SMTCoq indeed provide tactics to
> call SMT solvers. This is a recent work, so it currently requires the
> goal to be a Boolean, not a proposition (we are currently improving
> this). It is entirely safe and does not require classical logic.
>
> There is no Coq tactic as powerful as Sledgehammer in Coq. To my
> knowledge, the more powerful is what Claude presented, but it is indeed
> unsafe.
>
> Chantal.
>
>
>
> Le 03/04/2013 10:24, Arnaud Spiwack a écrit :
>> On interfacing external theorem provers with Coq in a safer manner, there
>> is recent work like this one: with
>> http://hal.inria.fr/docs/00/63/91/30/PDF/cpp11.pdf
>>
>>
>> On 3 April 2013 10:16, Jonathan Heras 
>> <jonathan.heras AT unirioja.es>
>>  wrote:
>>
>>> On 03/04/13 08:58, Claude Marche wrote:
>>>
>>>> Nevertheless, one should be aware of an important point: when the
>>>> external prover answers that the goal is valid, then the Why3 tactic
>>>> introduces an axiom in Coq to discharge the original goal. There is no 
>>>> Coq
>>>> proof generated. This is an important issue if you want to restrict your
>>>> trusted code base to the Coq kernel only. As far as I understand, this is
>>>> not a issue in Isabelle/sledgehammer since Isabelle does not build proof
>>>> terms internally (am I wrong ?)
>>>>
>>>
>>> In Isabelle, when the external prover answers that a goal is valid, it
>>> also returns the lemmas which have been used for that proof. Then, those
>>> lemmas are given as input to a program called Metis that tries to 
>>> reproduce
>>> the proof in Isabelle. In some cases, Metis cannot generate the proof even
>>> if external prover says that a goal is valid; in those cases, the goal is
>>> not admitted and in this way you always work with trusted code.
>>>
>>> Cheers,
>>> Jonathan
>>>
>>>
>>>
>>