| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 14:03:29 +0100 |
blanchet |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
file |
diff |
annotate
|
| Thu, 24 Oct 2013 12:43:33 +0200 |
blanchet |
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 22:10:57 +0200 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 09:50:48 +0200 |
blanchet |
adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 18:44:50 +0200 |
blanchet |
got rid of old error -- users who install SPASS manually are responsible for any version mismatches
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 10:26:56 +0200 |
blanchet |
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:30:31 +0200 |
blanchet |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
file |
diff |
annotate
|
| Sun, 26 May 2013 14:02:03 +0200 |
blanchet |
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
disabled choice in Satallax
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
prefer compiled version of LEO-II and Satallax if available
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
updated remote provers
|
file |
diff |
annotate
|
| Mon, 20 May 2013 11:27:13 +0200 |
blanchet |
started adding agsyHOL as an experimental prover
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Wed, 08 May 2013 15:47:19 +0200 |
blanchet |
use right default for "uncurried_aliases" with polymorphic SPASS
|
file |
diff |
annotate
|
| Fri, 03 May 2013 10:27:24 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 03 May 2013 10:26:34 +0200 |
blanchet |
pass certain readability-enhancing Vampire options only when an Isar proof is needed
|
file |
diff |
annotate
|
| Mon, 08 Apr 2013 12:11:06 +0200 |
blanchet |
robustness w.r.t. unknown arguments
|
file |
diff |
annotate
|
| Wed, 20 Mar 2013 15:35:35 +0100 |
blanchet |
use the right role for SPASS hypotheses
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 11:59:58 +0100 |
blanchet |
polymorphic SPASS is also SPASS
|
file |
diff |
annotate
|
| Thu, 21 Feb 2013 12:22:26 +0100 |
blanchet |
swap slices so that the last slice is more complete (for minimization)
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 15:26:19 +0100 |
blanchet |
upgraded to Alt-Ergo 0.95
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 10:45:01 +0100 |
blanchet |
turn off more evil Vampire options to facilitate Isar proof generation
|
file |
diff |
annotate
|
| Sun, 03 Feb 2013 17:31:33 +0100 |
blanchet |
tuned slicing (E-MaLeS and E-Par)
|
file |
diff |
annotate
|
| Sat, 02 Feb 2013 17:25:55 +0100 |
blanchet |
tune slices further
|
file |
diff |
annotate
|
| Sat, 02 Feb 2013 10:13:14 +0100 |
blanchet |
tweak ATP slices further
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
store fact filter along with ATP slice
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 17:55:02 +0100 |
blanchet |
make SPASS more configurable, for experiments
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 14:01:45 +0100 |
blanchet |
added E-Par support
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 20:55:32 +0100 |
blanchet |
tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
less verbose -- the warning will reach the users anyway by other means
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuned messages
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
added a timeout around script that relies on the network
|
file |
diff |
annotate
|
| Wed, 31 Oct 2012 11:23:21 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 16:09:45 +0200 |
blanchet |
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
|
file |
diff |
annotate
|
| Tue, 14 Aug 2012 15:23:28 +0200 |
blanchet |
tweak Vampire setup in the light of new evaluation
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 22:54:27 +0200 |
blanchet |
proper quoting
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 14:29:18 +0200 |
blanchet |
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 13:03:50 +0200 |
blanchet |
specify full path to clausifier
|
file |
diff |
annotate
|
| Mon, 06 Aug 2012 22:12:17 +0200 |
blanchet |
added iProver(-Eq) local
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 10:10:29 +0200 |
blanchet |
support older versions of Vampire
|
file |
diff |
annotate
|
| Thu, 02 Aug 2012 10:10:29 +0200 |
blanchet |
added E-MaLeS to list of provers for testing
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:34:33 +0200 |
blanchet |
tweaks in preparation for type encoding evaluation
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 08:52:40 +0200 |
blanchet |
extract Z3 unsat cores (for "z3_tptp")
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
don't ask E to generate a detailed proofs if not needed
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
pass more facts to LEO-II, in the light of latest evaluation
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
robust LEO-II setup that doesn't rely on ".leoatprc"
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
tweaked remote Vampire version
|
file |
diff |
annotate
|
| Mon, 28 May 2012 20:51:23 +0200 |
blanchet |
tweaked remote Vampire setup
|
file |
diff |
annotate
|
| Mon, 28 May 2012 20:45:28 +0200 |
blanchet |
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
|
file |
diff |
annotate
|
| Mon, 28 May 2012 20:25:38 +0200 |
blanchet |
don't generate definitions for LEO-II -- this cuases more harm than good
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:11:53 +0200 |
blanchet |
update Satallax setup based on evaluation
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:01:29 +0200 |
blanchet |
gracefully handle definition-looking premises
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
better handling of incomplete TSTP proofs
|
file |
diff |
annotate
|
| Wed, 23 May 2012 13:28:20 +0200 |
blanchet |
lower the monomorphization thresholds for less scalable provers
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
added one slice with configurable simplification turned off
|
file |
diff |
annotate
|
| Mon, 21 May 2012 11:31:52 +0200 |
blanchet |
invite users to upgrade their SPASS (so we can get rid of old code)
|
file |
diff |
annotate
|
| Mon, 21 May 2012 11:31:52 +0200 |
blanchet |
start phasing out old SPASS
|
file |
diff |
annotate
|
| Mon, 21 May 2012 11:31:52 +0200 |
blanchet |
minor tweak in Vampire setup
|
file |
diff |
annotate
|
| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
|
file |
diff |
annotate
|
| Mon, 14 May 2012 15:54:26 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
|
file |
diff |
annotate
|
| Sun, 13 May 2012 16:31:01 +0200 |
blanchet |
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
|
file |
diff |
annotate
|
| Thu, 10 May 2012 10:07:41 +0200 |
blanchet |
pass fewer facts to LEO-II and Satallax
|
file |
diff |
annotate
|
| Thu, 10 May 2012 10:07:40 +0200 |
blanchet |
tweak LEO-II setup
|
file |
diff |
annotate
|
| Thu, 10 May 2012 10:07:40 +0200 |
blanchet |
use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 13:18:55 +0200 |
blanchet |
tweak LEO-II setup
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 00:29:46 +0200 |
blanchet |
tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 20:55:09 +0200 |
blanchet |
removed confusing error
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 14:16:46 +0200 |
blanchet |
tried harder to make SML/NJ happy
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 11:15:49 +0200 |
blanchet |
tried to make SML/NJ happy
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 17:49:08 +0200 |
blanchet |
true delayed evaluation of "SPASS_VERSION" environment variable
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 13:54:31 +0200 |
blanchet |
more helpful error message
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 13:54:31 +0200 |
blanchet |
avoid option introduced in E 1.2 when invoking older versions of E
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 23:07:40 +0200 |
wenzelm |
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
tweak slices, based on eval by Daniel Wand
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
removed Satallax option, now that this is the default
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
improve "remote_satallax" by exploiting unsat core
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 16:53:24 +0100 |
blanchet |
generate weights and precedences for predicates as well
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 18:42:45 +0100 |
blanchet |
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 |
blanchet |
tweaks
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 13:53:09 +0100 |
blanchet |
added term_order option to Mirabelle
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 10:06:35 +0100 |
blanchet |
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 |
blanchet |
continued implementation of term ordering attributes
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
implement term order attribute (for experiments)
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
tuning -- don't refer to old, internal version number (needlessly confusing now)
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
more weight attribute tuning
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
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 |
blanchet |
internal renamings
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 00:44:30 +0100 |
blanchet |
renamed E weight attribute
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:35 +0100 |
blanchet |
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 |
blanchet |
don't report spurious LEO-II errors
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 18:58:33 +0100 |
blanchet |
better error message
|
file |
diff |
annotate
|
| Sat, 11 Feb 2012 13:41:36 +0100 |
blanchet |
new SPASS options
|
file |
diff |
annotate
|
| Fri, 10 Feb 2012 16:33:58 +0100 |
blanchet |
update SPASS slices
|
file |
diff |
annotate
|
| Thu, 09 Feb 2012 14:35:27 +0100 |
blanchet |
new SPASS slices
|
file |
diff |
annotate
|
| 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
|