| Wed, 17 Aug 2022 18:20:10 +0200 |
blanchet |
tweaked generation of Isar proofs
|
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
|
| Fri, 12 Aug 2022 15:35:07 +0200 |
blanchet |
added support for cvc5 (whose interface is almost identical to CVC4)
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 11:21:03 +0200 |
desharna |
tuned sledgehammer documentation
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 09:58:05 +0200 |
desharna |
added documentation
|
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 |
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
|