| 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
|
| Mon, 22 Feb 2021 15:24:04 +0100 |
wenzelm |
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
|
file |
diff |
annotate
|
| Wed, 16 Dec 2020 13:39:49 +0100 |
desharna |
enabled FOOL for E
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 18:45:19 +0100 |
desharna |
proper parsing of type encoding;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 15:11:37 +0100 |
desharna |
reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585
|
file |
diff |
annotate
|
| Thu, 19 Nov 2020 14:46:49 +0100 |
desharna |
repaired thf output broken by c7e2a9bdc585
|
file |
diff |
annotate
|
| Thu, 05 Nov 2020 18:14:02 +0100 |
desharna |
Added support for TFX to Sledgehammer
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:55:17 +0200 |
blanchet |
removed support for obsolete prover SNARK and underperforming prover E-Par
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:02:56 +0200 |
desharna |
tune filename
|
file |
diff |
annotate
| base
|