| Tue, 22 Jan 2019 17:22:09 +0100 |
blanchet |
tune ATP settings
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 02 Jul 2018 10:02:44 +0200 |
blanchet |
added option for noncommercial Vampire
|
file |
diff |
annotate
|
| Thu, 31 May 2018 10:59:36 +0200 |
blanchet |
more conservative output, avoiding nonstandard feature of E
|
file |
diff |
annotate
|
| Tue, 22 May 2018 17:15:02 +0200 |
blanchet |
added lambda-free HO output for Ehoh (higher-order E prototype)
|
file |
diff |
annotate
|
| Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:12:57 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2017 15:16:41 +0100 |
blanchet |
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 13:56:14 +0200 |
blanchet |
improved Vampire proof parser
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:21:07 +0200 |
blanchet |
use TFF0 with E 2.0 and above
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 10:40:40 +0200 |
blanchet |
updated remote Vampire version
|
file |
diff |
annotate
|
| Fri, 02 Sep 2016 11:26:52 +0200 |
blanchet |
adapted remote E
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Mon, 23 May 2016 18:04:45 +0200 |
blanchet |
generate Vampire 4.0 compatible output
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|
| Wed, 03 Dec 2014 17:08:24 +0100 |
blanchet |
prefer E 1.8, now that it's been tried and tested
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 14:18:07 +0200 |
blanchet |
use native encoding with Vampire -- modern versions handle types better than the old ones
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 12:29:52 +0200 |
blanchet |
added option to get cleaner SPASS proofs
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
pass options to remote Vampire
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 19:32:10 +0200 |
blanchet |
more precise handling of LEO-II skolemization
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:19 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:17 +0200 |
blanchet |
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
stick to external proofs when invoking E, because they are more detailed and do not merge steps
|
file |
diff |
annotate
|
| Sat, 12 Jul 2014 11:31:23 +0200 |
blanchet |
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:57 +0200 |
blanchet |
added 'dummy_thf_ml' prover for experiments with HOLyHammer
|
file |
diff |
annotate
|
| Tue, 17 Jun 2014 16:02:49 +0200 |
blanchet |
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:41:01 +0200 |
blanchet |
use right delimiters for Waldmeister proofs
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:41:00 +0200 |
blanchet |
added 'waldmeister_new' as ATP
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:39:41 +0200 |
blanchet |
give Z3 TPTP proofs a chance
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:18:15 +0200 |
fleury |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
use E 1.8's auto scheduler option
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:59 +0200 |
blanchet |
added missing space between command-line options
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 15:56:40 +0200 |
blanchet |
use Z3 TPTP cores rather than proofs since the latter are somewhat broken
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 11:49:47 +0200 |
blanchet |
improved parsing of "z3_tptp" proofs
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 17:16:02 +0200 |
blanchet |
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 17:00:14 +0200 |
blanchet |
use Alt-Ergo 0.95.2, the latest and greatest version
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 16:57:19 +0200 |
blanchet |
updated Z3 TPTP to 4.3.1+
|
file |
diff |
annotate
|
| 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
|