Email Gateway (Aug 18 2022 at 12:43): Email Gateway (Aug 18 2022 at 12:43):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
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.
smime.p7s
Email Gateway (Aug 18 2022 at 12:43):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
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:
Email Gateway (Aug 18 2022 at 12:43):From: Tobias Nipkow <nipkow@in.tum.de>
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:
vampire
Last updated: May 03 2024 at 04:19 UTC