The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Benedikt.AHRENS AT unice.fr
 wrote:
> Hello,
>
> on http://coq.inria.fr/about1-eng.html it says that Coq provides a 
> protocol for connecting with external theorem provers.
>
> I could not find any documentation for this in the reference manual. 
> Could somebody point out for me what I have overlooked, or give me a 
> hint where to find documentation for this feature?
>
> Thanks a lot in advance
> ben
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
For documentation, lookup "external" in the Global index of the Coq 
reference manual
(it should lead you to section 9.2).

For some time, Laurent Théry had a nice example available from his 
web-page (sos.zip).  It seems he removed it because the functionality is 
superseded by micromega, but you could ask him
to send you the example for inspiration.  It is about connecting with 
csdp to answer questions
about polynomial expressions being positive.

Laurent may also have other examples in his collections of developments.

It would be nice if we added an example of this on the Cocorico wiki.  
Any volunteer?

Yves