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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080813/d9d6d87f/attachment.diff
