| Tue, 25 Feb 2025 17:43:58 +0100 |
desharna |
tactic hammer documentation (from Jasmin)
|
file |
diff |
annotate
|
| Thu, 09 Jan 2025 13:18:37 +0100 |
Lukas Bartl |
tuned documentation and order of instantiated facts
|
file |
diff |
annotate
|
| Wed, 18 Dec 2024 11:02:56 +0100 |
desharna |
added documentation for new Sledehammer option "cache_dir"
|
file |
diff |
annotate
|
| Wed, 18 Dec 2024 10:43:44 +0100 |
desharna |
updated affiliation in Sledgehammer documentation
|
file |
diff |
annotate
|
| Thu, 31 Oct 2024 09:24:10 +0100 |
blanchet |
adjusted documentation
|
file |
diff |
annotate
|
| Fri, 25 Oct 2024 15:31:58 +0200 |
blanchet |
variable instantiation in Sledgehammer and Metis
|
file |
diff |
annotate
|
| Wed, 10 Apr 2024 11:44:25 +0200 |
wenzelm |
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;
|
file |
diff |
annotate
|
| Wed, 14 Jun 2023 15:47:27 +0200 |
blanchet |
disable 'falsify' and 'abduce' in Sledgehammer by default, since they don't seem to be very useful in practice
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
adopt terminology suggested by Larry Paulson
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
slightly more documentation
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
updated documentation
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| 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
|