Re: [isabelle] Which prover to use for Sledgehammer



Vampire is the best in many cases. It can be called remotely (thanks to
Fabian Immler and Makarius). They sent the perl script around some time
ago. I have attached it. I installed it where vampire should go:
isabelle/Distribution/contrib/vampire/x86-darwin (this is for the Mac).
It pretends to be vampire but calls Geoff Sutcliff's wonderful System on
TPTP http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP

Tobias

Christian Doczkal schrieb:
> Hi 
> 
> I now have the SPASS and E provers set up for use with sledgehammer and
> wanted to know whether there is any comparison or if there is anybody
> here who can tell me which prover solves more of your "every day work" 
> 
> Is there any other freely available and compatible ATP that one could
> try? Seems like Vampire would be a great tool but its not freely
> available.
> 

Attachment: vampire
Description: application/text



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.