Mon, 06 Feb 2012 23:01:01 +0100 |
blanchet |
renamed type encoding
|
file |
diff |
annotate
|
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
|
Tue, 06 Sep 2011 18:13:36 +0200 |
blanchet |
added dummy polymorphic THF system
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
cleaner "pff" dummy TFF0 prover
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
extended simple types with polymorphism -- the implementation still needs some work though
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added dummy PFF prover, for debugging purposes
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:34 +0200 |
blanchet |
first step towards polymorphic TFF + changed defaults for Vampire
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 01:18:48 +0200 |
blanchet |
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 23:55:21 +0200 |
blanchet |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 19:09:39 +0200 |
blanchet |
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 19:05:40 +0200 |
blanchet |
added one more known Z3 failure
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 22:12:30 +0200 |
blanchet |
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 23:18:13 +0200 |
blanchet |
fixed "hBOOL" of existential variables, and generate more helpers
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:37:23 +0200 |
blanchet |
always use TFF if possible
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:07:01 +0200 |
blanchet |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 15:50:27 +0200 |
blanchet |
updated known failures for Z3 3.0 TPTP
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 15:15:43 +0200 |
blanchet |
avoid TFF format with older Vampire versions
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
fixed TFF slicing
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
kindly ask Vampire to output axiom names
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
added formats to the slice and use TFF for remote Vampire
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
gracefully handle empty SPASS problems
|
file |
diff |
annotate
|
Wed, 17 Aug 2011 10:03:58 +0200 |
blanchet |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
support local HOATPs
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
LEO-II also supports FOF
|
file |
diff |
annotate
|
Tue, 09 Aug 2011 09:33:50 +0200 |
blanchet |
renamed E wrappers for consistency with CASC conventions
|
file |
diff |
annotate
|
Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
renamed "preds" encodings to "guards"
|
file |
diff |
annotate
|
Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
|
file |
diff |
annotate
|