| Wed, 28 Apr 2010 22:00:48 +0200 |
blanchet |
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 17:56:07 +0200 |
blanchet |
properly extract SPASS proof
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 17:47:30 +0200 |
blanchet |
try out Vampire 11 and parse its output correctly;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:32:45 +0200 |
blanchet |
removed "sorts" option, continued
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 18:58:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:17:41 +0200 |
blanchet |
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 11:38:46 +0200 |
blanchet |
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:36:49 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
| base
|