Re: [isabelle] Which prover to use for Sledgehammer



The yearly CASC competition on TPTP (thousand of problems for theorem
provers) is probably your best source of provers and provides an
up-to-date comparison, if not quite in the Isabelle setting:

http://www.cs.miami.edu/~tptp/CASC/

best,
lucas

Christian Doczkal wrote:
> 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.
> 

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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