Notes from Geoff Sutcliffe:
I added a few lines to the top of bin/isabelle ...
## Geoff makes Isabelle a robust tool, because he's kind
function cleanup {
rm -rf $HOME
}
if [ -z ${HOME+x} ]; then
HOME="/tmp/Isabelle_$$"
trap cleanup EXIT
fi
... which you might like to adopt. Now it works on SystemOnTPTP.
Notes to Geoff:
Once you have open the archive, Isabelle and its tool are ready to go. The
various tools are invoked as follows (given a file name %s):
Isabelle, competition version:
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle %s
Isabelle, demo version:
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot %s
Nitpick (formerly also called Nitrox):
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_nitpick %s
Refute:
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_refute %s
Here's an example:
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle $TPTP/Problems/SET/SET014^4.p
The output should look as follows:
running nitpick for 7 s
FAILURE: nitpick
running simp for 15 s
SUCCESS: simp
% SZS status Theorem
Additional sanity tests:
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/CSR/CSR150^3.p
STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/SYO/SYO304^5.p
The first problem is unprovable; the second one is proved by Satallax (after
some delay).
All the tools accept CNF, FOF, TFF0, TFF1, THF0, or THF1 problems and output
SZS statuses of the form
% SZS status XXX
where XXX is in the set
{Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}
Nitpick also output a model within "% SZS begin" and "% SZS end" tags, in
its idiosyncratic syntax. For TFF0 and THF0, phantom type arguments are not
supported, and type quantifiers are only allowed at the outermost position
in a formula, as "forall".
Enjoy!
Notes to myself:
I downloaded the official Isabelle2016-1 Linux package from
http://isabelle.in.tum.de/dist/Isabelle2016-1_linux.tar.gz
on "macbroy21" and renamed the directory "Isabelle2016-1-CASC". I modified
src/HOL/TPTP
to include changes backported from the development version of Isabelle. I
also modified "bin/isabelle" as suggested by Geoff above. I then built a
"HOL-TPTP" image:
./bin/isabelle build -b HOL-TPTP
I moved the heaps over to "./heaps":
mv ~/.isabelle/Isabelle2016-1/heaps .
I created some wrapper scripts in "./bin":
starexec_run_default
starexec_run_isabelle
starexec_run_isabelle_hot
starexec_run_nitpick
starexec_run_refute
I tested the "SET014^4" problem mentioned above.
Next, I installed and enabled ATPs.
LEO-II (1.6.2):
I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from
http://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v1.6.2.tgz
I did "make opt". I copied "bin/leo.opt" to
"~/Isabelle2016-1-CASC/contrib/leo".
I added this line to "etc/settings":
LEO2_HOME=$ISABELLE_HOME/contrib
Satallax (2.7):
I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved Satallax from
http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz
I added E to the path so that it gets detected by Satallax's configure
script:
export PATH=$PATH:~/Isabelle2013-CASC/contrib/e-1.6-2/x86-linux
I followed the instructions in "satallax-2.7/INSTALL". I copied
"bin/satallax.opt" to "~/Isabelle2013-CASC/contrib/satallax".
I added this line to "etc/settings":
SATALLAX_HOME=$ISABELLE_HOME/contrib
Vampire 4.0 (commit 2fedff6)
I copied the file "vampire", which I got from Giles Reger on 23 September
2015.
I added these lines to "etc/settings":
VAMPIRE_HOME=$ISABELLE_HOME/contrib
VAMPIRE_VERSION=4.0
Z3 TPTP (4.3.2.0 postrelease):
For Isabelle2015, I cloned out the git repository:
git clone https://git01.codeplex.com/z3
I build Z3 and from "build", ran "make examples" to build "z3_tptp".
I copied "z3_tptp" as "z3_tptp-solver" and "libz3.so" to "./contrib",
and put a wrapper called "z3_tptp" to set the library path correctly
(inspired by the CVC4 setup on Mac OS X).
I added this line to "etc/settings":
Z3_TPTP_HOME=$ISABELLE_HOME/contrib
Unfortunately, I got "z3::exception" errors. I did not investigate this
further and commented out the environment variable in "etc/settings".
To test that the examples actually worked, I create a file called
"/tmp/T.thy" with the following content:
theory T imports Main begin
lemma "a = b ==> [b] = [a]"
sledgehammer [cvc4 e leo2 satallax spass vampire z3 (*z3_tptp*)] ()
oops
end
Then I ran
./bin/isabelle process -T /tmp/T
I also performed the aforementioned sanity tests.
Finally, I renamed "README" to "README.orig" and copied this "ReadMe" over.
Ideas for a future year:
* Unfold definitions, esp. if it makes the problem more first-order (cf.
"SEU466^1").
* Detect and remove needless definitions.
That's it.
Jasmin Blanchette
15 December 2016
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
