The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

FYI, http://focal.inria.fr/zenon/ is an ATP that can generate Coq proofs. But I don't know if there is an interface to call it from Coq.

Regards,

Frederic.

Le 02/04/2013 18:57, Erik Parmann a écrit :

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.