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:


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.