| Sun, 05 Feb 2012 13:28:51 +0100 |
blanchet |
remove option that's on by default
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 12:27:10 +0100 |
blanchet |
no need for a script/mega-hack with the new SPASS
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 12:27:10 +0100 |
blanchet |
cleaned up new SPASS parsing
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
made option available to users (mostly for experiments)
|
file |
diff |
annotate
|
| Fri, 03 Feb 2012 18:00:55 +0100 |
blanchet |
optimization: slice caching in case two consecutive slices are nearly identical
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 15:14:18 +0100 |
blanchet |
change 9ce354a77908 wasn't quite right -- here's an improvement
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 12:51:03 +0100 |
blanchet |
better SPASS setup
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 12:42:05 +0100 |
blanchet |
include new SPASS by default if available
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 17:09:08 +0100 |
blanchet |
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 16:11:15 +0100 |
blanchet |
improve SPASS setup
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 15:10:03 +0100 |
blanchet |
fixed syntax bug in DFG output
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 14:39:21 +0100 |
blanchet |
new SPASS setup
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:18:58 +0100 |
blanchet |
new SPASS setup
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 17:15:59 +0100 |
blanchet |
rename lambda translation schemes
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 18:07:32 +0100 |
blanchet |
SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 17:06:14 +0100 |
blanchet |
give each time slice its own lambda translation
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 11:16:37 +0100 |
blanchet |
renamed experimental systems
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 15:05:59 +0000 |
blanchet |
document new experimental provers
|
file |
diff |
annotate
|
| Fri, 04 Nov 2011 15:05:58 +0000 |
blanchet |
added remote iProver(-Eq) for experimentation
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
|
file |
diff |
annotate
|
| Fri, 21 Oct 2011 12:44:20 +0200 |
blanchet |
disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 21:40:32 +0200 |
blanchet |
one more LEO-II failure
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 16:36:13 +0200 |
blanchet |
more uniform SZS status handling
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 21:37:37 +0200 |
blanchet |
parse Satallax unsat cores
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tweaking polymorphic TFF and THF output
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
file |
diff |
annotate
|