| 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
|