| Thu, 29 Apr 2010 17:31:08 +0200 |
blanchet |
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
|
changeset |
files
|
| Thu, 29 Apr 2010 13:41:51 +0200 |
blanchet |
redo more Metis/Sledgehammer example
|
changeset |
files
|
| Thu, 29 Apr 2010 12:21:20 +0200 |
blanchet |
fixed definition of "bad frees" so that it actually works
|
changeset |
files
|
| Thu, 29 Apr 2010 11:38:23 +0200 |
blanchet |
don't remove last line of proof
|
changeset |
files
|
| Thu, 29 Apr 2010 11:22:24 +0200 |
blanchet |
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
|
changeset |
files
|
| Thu, 29 Apr 2010 10:55:59 +0200 |
blanchet |
make SML/NJ happy, take 2
|
changeset |
files
|
| Thu, 29 Apr 2010 10:25:26 +0200 |
blanchet |
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
|
changeset |
files
|
| Thu, 29 Apr 2010 01:17:14 +0200 |
blanchet |
expand combinators in Isar proofs constructed by Sledgehammer;
|
changeset |
files
|
| Thu, 29 Apr 2010 01:11:06 +0200 |
blanchet |
more neg_clausify proofs that get replaced by direct proofs
|
changeset |
files
|
| Wed, 28 Apr 2010 22:36:39 +0200 |
blanchet |
redo some of the metis proofs
|
changeset |
files
|
| Wed, 28 Apr 2010 22:00:48 +0200 |
blanchet |
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
|
changeset |
files
|
| Wed, 28 Apr 2010 21:59:29 +0200 |
blanchet |
improve unskolemization
|
changeset |
files
|