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



This could be interesting not just for developers.

Tobias

-------- Original Message --------
Subject: [isabelle-dev]  ATP Vampire via internet / vampire for Mac
Date: Wed, 13 Aug 2008 19:14:18 +0200
From: Fabian Immler <immler at in.tum.de>
To: isabelle-dev at mailbroy.informatik.tu-muenchen.de

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

#! /usr/bin/perl -w
#
# Vampire-Wrapper
# ---------------
#
# - querys a Vampire theorem prover on SystemOnTPTP
#   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
# - behaves like a locally installed Vampire
# => can be used for Isabelle(2008) when Vampire is not available (e.g. on a Mac)
# 
# Installation:
# - just put this file to the place where Isabelle expects the vampire-executable
#   (VAMPIRE_HOME). Default is $ISABELLE_HOME/contrib/vampire/$ML_PLATFORM/
#   
# Problems, questions, suggestions to: immler at in.tum.de
#
use strict "vars";
use Getopt::Std;
use HTTP::Request::Common;
use LWP::UserAgent;

# address of proof-server
my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";;

#name of prover and its executable on the server, e.g.
# Vampire---9.0
# jumpirefix
my $prover = "Vampire---9.0";
my $command = "jumpirefix";

# pass arguments
my $options = "";
while(scalar(@ARGV)>1){
	$options.=" ".shift(@ARGV);
}
# last argument is problemfile to be uploaded
my $problem = [shift(@ARGV)];

# fill in form
my %URLParameters = (
    "NoHTML" => 1,
    "QuietFlag" => "-q01",
    "SubmitButton" => "RunSelectedSystems",
    "ProblemSource" => "UPLOAD",
    "UPLOADProblem" => $problem,
    "System___$prover" => "$prover",
    "Format___$prover" => "tptp",
    "Command___$prover" => "$command $options %s"
);

# Query Server
my $Agent = LWP::UserAgent->new;
my $Request = POST($SystemOnTPTPFormReplyURL,
	Content_Type => 'form-data',Content => \%URLParameters);
my $Response = $Agent->request($Request);
    
#catch errors, let isabelle/watcher know
if($Response->is_success){
	print $Response->content;
} else {
	print $Response->message;
	print "\nCANNOT PROVE\n";
}

_______________________________________________
Isabelle-dev mailing list
Isabelle-dev at mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.