| Mon, 17 Oct 2022 13:04:00 +0200 |
blanchet |
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
|
file |
diff |
annotate
|
| Sat, 17 Sep 2022 16:50:39 +0200 |
wenzelm |
proper file headers;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 15:09:53 +0200 |
blanchet |
tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s
|
file |
diff |
annotate
|
| Tue, 02 Aug 2022 13:23:57 +0200 |
blanchet |
changed the order of Zipperposition slices in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 27 May 2022 13:46:40 +0200 |
desharna |
excluded dummy ATPs from Sledgehammer's default provers
|
file |
diff |
annotate
|
| Wed, 13 Apr 2022 16:53:46 +0200 |
blanchet |
pass new option only to new version of E
|
file |
diff |
annotate
|
| Fri, 08 Apr 2022 17:17:21 +0200 |
blanchet |
enable an E option suggested by Petar Vukmirovic
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 18:14:11 +0200 |
blanchet |
further tweaked E's setup
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 15:26:18 +0200 |
blanchet |
tweaked E setup
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
further modernized E setup
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
cleaned up obsolete E setup and a bit of SPASS
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
|
file |
diff |
annotate
|
| Wed, 02 Feb 2022 13:34:52 +0100 |
blanchet |
enable induction in one of Zipperposition's slices
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 12:49:14 +0100 |
blanchet |
don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
removed experimental prover z3_tptp
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
run all installed provers by default
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
further work on new Sledgehammer slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
removed obscure E option
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalize slicing format
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
thread slices through
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
simplified 'best_slice' data structure and made minor changes to slices
|
file |
diff |
annotate
|
| Fri, 21 Jan 2022 21:09:55 +0100 |
desharna |
proper fact filter for dummy ATPs
|
file |
diff |
annotate
|
| Wed, 05 Jan 2022 10:56:41 +0100 |
desharna |
removed $ite from E 2.6 in THF format
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 23:17:08 +0100 |
desharna |
used TH1 for Leo-III in sledgehammer
|
file |
diff |
annotate
|
| Fri, 19 Nov 2021 11:04:53 +0100 |
desharna |
proper polymorphism for TH1 format in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 19 Nov 2021 10:53:22 +0100 |
desharna |
refactored $ite and $let configuration and added dummy_thf_reduced prover
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 00:10:16 +0100 |
desharna |
separated FOOL from $ite/$let in TPTP output
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Thu, 14 Oct 2021 16:56:02 +0200 |
desharna |
tuned Vampire configuration to use TFX in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 04 Oct 2021 10:17:11 +0200 |
desharna |
tuned zipperposition config in sledgehammer
|
file |
diff |
annotate
|
| Wed, 29 Sep 2021 16:47:53 +0200 |
desharna |
tuned Zipperposition slides in sledgehammer
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 12:35:43 +0200 |
desharna |
updated to Zipperposition 2.1
|
file |
diff |
annotate
|
| Wed, 22 Sep 2021 12:41:40 +0200 |
desharna |
removed checks for non-commercial usage of Vampire as it is now under BSD licence
|
file |
diff |
annotate
|
| Wed, 22 Sep 2021 12:25:09 +0200 |
desharna |
enabled FOOL for Vampire in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 22 Sep 2021 10:46:42 +0200 |
desharna |
used Vampire 4.5.1 in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 Sep 2021 16:02:04 +0200 |
wenzelm |
clarified name and options for old vampire-4.2.2;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2021 14:29:02 +0200 |
blanchet |
handle Zipperposition's ResourceOut gracefully
|
file |
diff |
annotate
|
| Fri, 27 Aug 2021 14:28:56 +0200 |
blanchet |
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
|
file |
diff |
annotate
|
| Wed, 04 Aug 2021 08:23:12 +0200 |
desharna |
added dummy_fof prover to Sledgehammer
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 09:22:38 +0200 |
desharna |
added dummy_thf prover to Sledgehammer
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 14:47:52 +0200 |
blanchet |
tuned E's lambda encoding
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 10:38:14 +0200 |
blanchet |
use Vampire's clausifier with iProver, now that E's is no longer supported
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 15:27:55 +0200 |
blanchet |
get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options
|
file |
diff |
annotate
|
| Tue, 13 Jul 2021 10:57:14 +0200 |
blanchet |
wait for E 2.7 before using 'ite' in HO mode
|
file |
diff |
annotate
|
| Tue, 13 Jul 2021 10:57:14 +0200 |
blanchet |
added alternative E binary name
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 16:30:15 +0200 |
blanchet |
adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 12:57:22 +0200 |
desharna |
added support for TFX's and THF's $ite to Sledgehammer
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 22:16:31 +0200 |
wenzelm |
clarified signature: more structured arguments, notably for remote provers;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 21:41:28 +0100 |
wenzelm |
proper shell quote;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 21:02:34 +0100 |
wenzelm |
removed spurious references to perl / libwww-perl;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 20:29:26 +0100 |
wenzelm |
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 16:50:11 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2021 15:14:46 +0100 |
wenzelm |
use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 11:06:39 +0100 |
desharna |
tuned best_slices in atp_config
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 10:10:44 +0100 |
desharna |
tuned exec field in atp_config
|
file |
diff |
annotate
|
| Tue, 23 Feb 2021 12:20:50 +0100 |
desharna |
proper usage of hypotheses for zipperposition's TPTP generation
|
file |
diff |
annotate
|
| Tue, 23 Feb 2021 10:13:09 +0100 |
desharna |
merged
|
file |
diff |
annotate
|
| Fri, 12 Feb 2021 11:18:12 +0100 |
desharna |
proper prover capabilities for zipperposition
|
file |
diff |
annotate
|