coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Sledgehammer for Coq?

From: Erik Parmann <epa095 AT uib.no>
To: coq-club AT inria.fr
Subject: [Coq-Club] Sledgehammer for Coq?
Date: Tue, 2 Apr 2013 12:57:53 +0200

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.

[Coq-Club] Sledgehammer for Coq?, Erik Parmann, 04/02/2013
- Re: [Coq-Club] Sledgehammer for Coq?, Kristopher Micinski, 04/02/2013
  - Re: [Coq-Club] Sledgehammer for Coq?, Claude Marche, 04/03/2013
    - Re: [Coq-Club] Sledgehammer for Coq?, Jonathan Heras, 04/03/2013
      - Re: [Coq-Club] Sledgehammer for Coq?, Arnaud Spiwack, 04/03/2013
        
        Re: [Coq-Club] Sledgehammer for Coq?, Chantal Keller, 04/03/2013
        
        Re: [Coq-Club] Sledgehammer for Coq?, Gabriel Scherer, 04/04/2013
        
        Re: [Coq-Club] Sledgehammer for Coq?, Kristopher Micinski, 04/04/2013
- Re: [Coq-Club] Sledgehammer for Coq?, Frederic Blanqui, 04/03/2013