author | blanchet |
Tue, 21 May 2013 11:01:14 +0200 | |
changeset 52098 | 6c38df1d294a |
child 52123 | 8a34b9a882bb |
permissions | -rw-r--r-- |
52098
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
1 |
Isabelle/HOL 2013 at CASC-24 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
2 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
3 |
Notes to Geoff: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
4 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
5 |
Once you have open the archive, Isabelle and its tool are ready to go. The |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
6 |
various tools are invoked as follows: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
7 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
8 |
Isabelle, competition version: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
9 |
./bin/isabelle tptp_isabelle %d %s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
10 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
11 |
Isabelle, demo version: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
12 |
./bin/isabelle tptp_isabelle_hot %d %s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
13 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
14 |
Nitpick and Nitrox: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
15 |
./bin/isabelle tptp_nitpick %d %s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
16 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
17 |
Refute: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
18 |
./bin/isabelle tptp_refute %d %s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
19 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
20 |
Here's an example: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
21 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
22 |
./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SET/SET014^4.p |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
23 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
24 |
The output should look as follows: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
25 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
26 |
> val it = (): unit |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
27 |
val commit = fn: unit -> bool |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
28 |
Loading theory "Scratch_tptp_isabelle_hot_29414_2568" |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
29 |
running nitpick for 7 s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
30 |
FAILURE: nitpick |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
31 |
running simp for 15 s |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
32 |
SUCCESS: simp |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
33 |
% SZS status Theorem |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
34 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
35 |
Additional sanity tests: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
36 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
37 |
./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/CSR/CSR150^3.p |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
38 |
./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/SYO/SYO304^5.p |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
39 |
./bin/isabelle tptp_isabelle_hot 300 $TPTP/Problems/PUZ/PUZ087^1.p |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
40 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
41 |
The first problem is unprovable; the second one is proved by Satallax; the |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
42 |
third one is proved by LEO-II. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
43 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
44 |
All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS statuses |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
45 |
of the form |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
46 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
47 |
% SZS status XXX |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
48 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
49 |
where XXX is in the set |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
50 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
51 |
{Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable} |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
52 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
53 |
Nitpick and Nitrox also output a model within "% SZS begin" and "% SZS end" |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
54 |
tags. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
55 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
56 |
In 2011, there were some problems with Java (needed for Nitpick), because it |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
57 |
required so much memory at startup. I doubt there will be any problems this |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
58 |
year, because Isabelle now includes its own version of Java, but the solution |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
59 |
back then was to replace |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
60 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
61 |
exec "$ISABELLE_TOOL" java |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
62 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
63 |
in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
64 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
65 |
/usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
66 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
67 |
See the emails we exchanged on July 18, 2011, with the subject "No problem on |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
68 |
my Linux 64-bit". |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
69 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
70 |
Enjoy! |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
71 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
72 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
73 |
Notes to myself: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
74 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
75 |
I downloaded the official Isabelle2013 Linux package from |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
76 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
77 |
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013_linux.tar.gz |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
78 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
79 |
on a "macbroy" machine and renamed the directory "Isabelle2013-CASC". I built |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
80 |
a "HOL-TPTP" image: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
81 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
82 |
./bin/isabelle build -b HOL-TPTP |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
83 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
84 |
I copied the heaps over to "./heaps": |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
85 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
86 |
mv ~/.isabelle/Isabelle2013/heaps . |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
87 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
88 |
To use this image and suppress some scary output, I added |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
89 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
90 |
HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val it = (): unit" |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
91 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
92 |
to the next-to-last lines of "src/HOL/TPTP/lib/Tools/tptp_[inrs]*". |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
93 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
94 |
At this point I tested the "SYN044^4" mentioned above. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
95 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
96 |
I renamed "README" to "README.orig" and copied this "ReadMe" over. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
97 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
98 |
Next, I installed and enabled ATPs. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
99 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
100 |
LEO-II (1.4.3): |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
101 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
102 |
I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved LEO-II from |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
103 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
104 |
http://www.ags.uni-sb.de/~leo/leo2_v1.4.3.tgz |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
105 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
106 |
I did "make opt". I copied |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
107 |
"bin/leo.opt" to "~/Isabelle2013-CASC/contrib/leo". |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
108 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
109 |
I added this line to "etc/settings": |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
110 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
111 |
LEO2_HOME=$ISABELLE_HOME/contrib |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
112 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
113 |
Satallax (2.7): |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
114 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
115 |
I logged to a 32-bit Linux ("lxlabbroy") machine. I retrieved Satallax from |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
116 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
117 |
http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/satallax-2.7.tar.gz |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
118 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
119 |
I added E to the path so that it gets detected by Satallax's configure |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
120 |
script: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
121 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
122 |
export PATH=$PATH:~/Isabelle2013-CASC/contrib/e-1.6-2/x86-linux |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
123 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
124 |
I followed the instructions in "satallax-2.7/INSTALL". I copied |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
125 |
"bin/satallax.opt" to "~/Isabelle2013-CASC/contrib/satallax". |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
126 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
127 |
I added this line to "etc/settings": |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
128 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
129 |
SATALLAX_HOME=$ISABELLE_HOME/contrib |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
130 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
131 |
Vampire (2.6): |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
132 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
133 |
I copied the file "vampire_rel.linux64" from the 2012 CASC archive to |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
134 |
"~/Isabelle2013-CASC/contrib/vampire". |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
135 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
136 |
I added these lines to "etc/settings": |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
137 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
138 |
VAMPIRE_HOME=$ISABELLE_HOME/contrib |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
139 |
VAMPIRE_VERSION=2.6 |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
140 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
141 |
Z3 (3.2): |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
142 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
143 |
I uncommented the following line in "contrib/z3-3.2/etc/settings": |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
144 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
145 |
# Z3_NON_COMMERCIAL="yes" |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
146 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
147 |
To test that the examples actually worked, I did |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
148 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
149 |
./bin/isabelle tty |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
150 |
theory T imports Main begin; |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
151 |
lemma "a = b ==> [b] = [a]"; |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
152 |
sledgehammer [e leo2 satallax spass vampire z3 z3_tptp] (); |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
153 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
154 |
and I performed the aforementioned sanity tests. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
155 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
156 |
Ideas for next year: |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
157 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
158 |
* Unfold definitions, esp. if it makes the problem more first-order (cf. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
159 |
"SEU466^1"). |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
160 |
* Detect and remove needless definitions. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
161 |
* Expand "p b" to "(b & p True) | (~ b & p False)" (cf. "CSR148^3"). |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
162 |
* Select subset of axioms (cf. "CSR148^3"). |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
163 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
164 |
That's it. |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
165 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
166 |
|
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
167 |
Jasmin Blanchette |
6c38df1d294a
added CASC-related files, to keep a public record of the Isabelle submission at the competition
blanchet
parents:
diff
changeset
|
168 |
21 May 2013 |