| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
implemented 'max_proofs' mechanism
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
document new option 'max_proofs'
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
updated documentation of 'slice' (now 'slices') option
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
revised Sledgehammer documentation
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
generalized the 'slice' option towards more flexible slicing
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 22:07:04 +0100 |
desharna |
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
|
file |
diff |
annotate
|
| Mon, 20 Dec 2021 08:40:28 +0100 |
desharna |
updated Mirabelle documentation
|
file |
diff |
annotate
|
| Mon, 20 Dec 2021 08:14:41 +0100 |
desharna |
proper documentation for induction_rules Sledgehammer option
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 11:11:44 +0200 |
desharna |
fixed veriT environment variable in sledgehammer's documentation
|
file |
diff |
annotate
|
| Mon, 27 Sep 2021 11:19:56 +0200 |
blanchet |
tuned docs
|
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
|
| Thu, 29 Jul 2021 17:08:46 +0200 |
desharna |
documented Mirabelle_Sledgehammer's new keep semantics
|
file |
diff |
annotate
|
| Wed, 28 Jul 2021 14:16:19 +0200 |
desharna |
added automatic uniform stride option to Mirabelle
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 14:47:52 +0200 |
blanchet |
removed setup for outdated CVC3 from Isabelle
|
file |
diff |
annotate
|
| Mon, 19 Jul 2021 10:37:48 +0200 |
blanchet |
updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain
|
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
|
| 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, 08 Jul 2021 17:43:35 +0200 |
desharna |
documented Sledgehammer option "induction_rules"
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 15:10:52 +0200 |
desharna |
added documentation for changes to Sledgehammer option "lam_trans"
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
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
|
| Thu, 17 Jun 2021 11:27:21 +0200 |
desharna |
tuned Mirabelle documentation
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 10:46:27 +0200 |
desharna |
shortened long lines
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 10:43:53 +0200 |
desharna |
fixed typos
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 10:37:29 +0200 |
desharna |
updated Mirabelle documentation
|
file |
diff |
annotate
|
| Tue, 18 May 2021 15:17:55 +0200 |
wenzelm |
option document_logo;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2021 10:11:11 +0200 |
wenzelm |
simplified typesetting of \<guillemotleft>...\<guillemotright>;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 21:02:34 +0100 |
wenzelm |
removed spurious references to perl / libwww-perl;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 16:44:29 +0100 |
desharna |
Tuned documentation
|
file |
diff |
annotate
|
| Thu, 05 Nov 2020 19:01:25 +0100 |
desharna |
Expanded and tuned documentation
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 18:23:27 +0200 |
blanchet |
tuned mirabelle documentation
|
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:47:35 +0200 |
blanchet |
removed spurious documentation item
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Tue, 08 Sep 2020 11:32:57 +0200 |
desharna |
[mirabelle] add initial documentation in Sledgehammer's doc
|
file |
diff |
annotate
|
| Mon, 28 Sep 2020 16:23:15 +0200 |
wenzelm |
obsolete, T1 fonts are fine in lualatex (see also cc71f01f9fde);
|
file |
diff |
annotate
|
| Thu, 20 Aug 2020 11:52:46 +0200 |
blanchet |
basic integration of Zipperposition 2.0
|
file |
diff |
annotate
|
| Wed, 10 Jun 2020 15:55:41 +0200 |
blanchet |
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:59:25 +0200 |
blanchet |
added support for Zipperposition on SystemOnTPTP
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:23:14 +0200 |
blanchet |
removed support for old system E-MaLeS
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:18:06 +0200 |
blanchet |
added support for repote Alt-Ergo
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:05:03 +0200 |
blanchet |
updated nomenclature for TPTP languages to use modern three-symbol abbreviations (e.g. TF1)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:59:56 +0200 |
blanchet |
removed support for E-ToFoF, which has lost its raison d'etre since E 2.0 supports TF0
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:55:14 +0200 |
blanchet |
removed E-SInE, a very old system by now (and SInE has been incorporated in many provers in the past decade)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:51:16 +0200 |
blanchet |
removed support for iProver-Eq
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:47:42 +0200 |
blanchet |
updated iProver setup and tuned other ATP setups
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:06:02 +0200 |
blanchet |
removed support for remote Satallax because its output does not clearly identify the lemmas used
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 13:25:30 +0200 |
blanchet |
changed Satallax's setup to invoke E
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 16:59:37 +0200 |
blanchet |
updated veriT part of Sledgehammer documentation
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 16:37:52 +0200 |
blanchet |
added para constrasting 'primrec' and 'fun' -- and removed my middle name
|
file |
diff |
annotate
|
| Wed, 18 Jul 2018 16:44:01 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Mon, 02 Jul 2018 10:17:23 +0200 |
blanchet |
update Sledgehammer docs w.r.t. Vampire
|
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
|
| Tue, 07 Nov 2017 15:16:41 +0100 |
blanchet |
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
|
file |
diff |
annotate
|
| Sat, 30 Sep 2017 22:55:23 +0200 |
blanchet |
updated Sledgehammer docs
|
file |
diff |
annotate
|
| Mon, 07 Aug 2017 11:21:07 +0200 |
blanchet |
use TFF0 with E 2.0 and above
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 16:21:29 +0200 |
blanchet |
removed French accent from docs
|
file |
diff |
annotate
|
| Tue, 30 Aug 2016 16:39:47 +0200 |
blanchet |
tuned docs
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
updated Sledgehammer documentation
|
file |
diff |
annotate
|