| Wed, 21 Mar 2012 16:53:24 +0100 |
improve "remote_satallax" by exploiting unsat core
|
file | diff | annotate |
| Wed, 21 Mar 2012 16:53:24 +0100 |
generate weights and precedences for predicates as well
|
file | diff | annotate |
| Tue, 20 Mar 2012 18:42:45 +0100 |
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
|
file | diff | annotate |
| Tue, 20 Mar 2012 18:42:45 +0100 |
tweaks
|
file | diff | annotate |
| Tue, 20 Mar 2012 13:53:09 +0100 |
added term_order option to Mirabelle
|
file | diff | annotate |
| Tue, 20 Mar 2012 10:06:35 +0100 |
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
continued implementation of term ordering attributes
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
implement term order attribute (for experiments)
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
tuning -- don't refer to old, internal version number (needlessly confusing now)
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
more weight attribute tuning
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
internal renamings
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
renamed E weight attribute
|
file | diff | annotate |
| Fri, 24 Feb 2012 11:23:35 +0100 |
added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
|
file | diff | annotate |
| Tue, 14 Feb 2012 20:13:07 +0100 |
don't report spurious LEO-II errors
|
file | diff | annotate |
| Tue, 14 Feb 2012 18:58:33 +0100 |
better error message
|
file | diff | annotate |
| Sat, 11 Feb 2012 13:41:36 +0100 |
new SPASS options
|
file | diff | annotate |
| Fri, 10 Feb 2012 16:33:58 +0100 |
update SPASS slices
|
file | diff | annotate |
| Thu, 09 Feb 2012 14:35:27 +0100 |
new SPASS slices
|
file | diff | annotate |
| Mon, 06 Feb 2012 23:01:01 +0100 |
renamed type encoding
|
file | diff | annotate |
| Sun, 05 Feb 2012 13:28:51 +0100 |
remove option that's on by default
|
file | diff | annotate |
| Sun, 05 Feb 2012 12:27:10 +0100 |
no need for a script/mega-hack with the new SPASS
|
file | diff | annotate |
| Sun, 05 Feb 2012 12:27:10 +0100 |
cleaned up new SPASS parsing
|
file | diff | annotate |
| Sat, 04 Feb 2012 12:08:18 +0100 |
made option available to users (mostly for experiments)
|
file | diff | annotate |
| Fri, 03 Feb 2012 18:00:55 +0100 |
optimization: slice caching in case two consecutive slices are nearly identical
|
file | diff | annotate |
| Thu, 02 Feb 2012 15:14:18 +0100 |
change 9ce354a77908 wasn't quite right -- here's an improvement
|
file | diff | annotate |
| Thu, 02 Feb 2012 12:51:03 +0100 |
better SPASS setup
|
file | diff | annotate |
| Thu, 02 Feb 2012 12:42:05 +0100 |
include new SPASS by default if available
|
file | diff | annotate |
| Tue, 31 Jan 2012 17:09:08 +0100 |
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 |
improve SPASS setup
|
file | diff | annotate |
| Tue, 31 Jan 2012 15:10:03 +0100 |
fixed syntax bug in DFG output
|
file | diff | annotate |
| Tue, 31 Jan 2012 14:39:21 +0100 |
new SPASS setup
|
file | diff | annotate |
| Mon, 30 Jan 2012 17:18:58 +0100 |
new SPASS setup
|
file | diff | annotate |
| Mon, 30 Jan 2012 17:15:59 +0100 |
rename lambda translation schemes
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Wed, 14 Dec 2011 18:07:32 +0100 |
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 |
give each time slice its own lambda translation
|
file | diff | annotate |
| Sun, 06 Nov 2011 11:16:37 +0100 |
renamed experimental systems
|
file | diff | annotate |
| Fri, 04 Nov 2011 15:05:59 +0000 |
document new experimental provers
|
file | diff | annotate |
| Fri, 04 Nov 2011 15:05:58 +0000 |
added remote iProver(-Eq) for experimentation
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
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 |
added DFG unsorted support (like in the old days)
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
added sorted DFG output for coming version of SPASS
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
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 |
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 |
one more LEO-II failure
|
file | diff | annotate |
| Wed, 19 Oct 2011 16:36:13 +0200 |
more uniform SZS status handling
|
file | diff | annotate |
| Mon, 17 Oct 2011 21:37:37 +0200 |
parse Satallax unsat cores
|
file | diff | annotate |
| Wed, 07 Sep 2011 13:50:17 +0200 |
tweaking polymorphic TFF and THF output
|
file | diff | annotate |
| Wed, 07 Sep 2011 09:10:41 +0200 |
rationalize uniform encodings
|
file | diff | annotate |
| Tue, 06 Sep 2011 18:13:36 +0200 |
added dummy polymorphic THF system
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:46 +0200 |
cleaner "pff" dummy TFF0 prover
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
extended simple types with polymorphism -- the implementation still needs some work though
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
added dummy PFF prover, for debugging purposes
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:34 +0200 |
first step towards polymorphic TFF + changed defaults for Vampire
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
improved handling of induction rules in Sledgehammer
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
added generation of induction rules
|
file | diff | annotate |
| Fri, 26 Aug 2011 01:18:48 +0200 |
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 |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
file | diff | annotate |
| Thu, 25 Aug 2011 22:05:18 +0200 |
make TFF output less explicit where possible
|
file | diff | annotate |