[isabelle-dev] ATP Vampire via internet / vampire for Mac
immler at in.tum.de
Wed Aug 13 19:14:18 CEST 2008
in the context of my work as student assistant, the following (for some
of you perhaps useful) perl-script was developed:
It can be used if you cannot install Vampire(for the
sledgehammer-tool)on your machine for instance if you use a Mac.
The script queries a proof-server
(http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP) to solve problems
and passes the solutions to isabelle.
Isabelle can use this script the same way it uses a locally installed
So installation is similar to the installation of the 'real' vampire as
described here: http://isabelle.in.tum.de/sledgehammer.html
Just use the attached script (named vampire) instead of the prover
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev