The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Interesting that there hasn't been any work on this: it was my
intuition that someone *had* done this (I look forward to someone here
to pointing me to better refs if has been indeed done).  The best of
which I know is:

@MISC{Ayache06combiningthe,
    author = {Nicolas Ayache},
    title = {Combining the Coq proof assistant with first-order
decision procedures},
    year = {2006}
}

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.4549

and

Connecting a Logical Framework to a First-Order Logic Prover
http://www.cse.chalmers.se/~ulfn/papers/fol.pdf

Kris

On Tue, Apr 2, 2013 at 6:57 AM, Erik Parmann 
<epa095 AT uib.no>
 wrote:
> Hi,
> I have been playing with both Coq and Isabelle lately, and especially with
> the sledgehammer[1] tool for the latter. It can at times be quite useful,
> and in many ways change the way I develop proofs. This raised the question
> of why there is no equivalent for Coq. Is it just that no-one has had the
> time to develop it, or are there deeper reasons, either technical or
> "cultural"?
>
>
> 1: http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html
>
> Thanks,
> --
> Erik Parmann
> University of Bergen, Norway.