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:
> 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
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