[isabelle-dev] ATP Vampire via internet / vampire for Mac

[Fabian Immler]

Dear all,

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 
Vampire.

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 
executable.


Fabian Immler
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: vampire
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080813/d9d6d87f/attachment.ksh>