| Mon, 26 Feb 2024 13:10:37 +0100 |
blanchet |
deal with new-style Vampire skolemization in reconstructed Isar proofs
|
file |
diff |
annotate
|
| Wed, 06 Dec 2023 14:05:18 +0100 |
blanchet |
check that Isar proofs contain one 'show'
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 17:16:32 +0200 |
blanchet |
added argo
|
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 |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Mon, 22 Aug 2022 06:27:28 +0200 |
Mathias Fleury |
remove duplicate parsing for alethe; fix skolemization;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 18:20:10 +0200 |
blanchet |
tweaked generation of Isar proofs
|
file |
diff |
annotate
|
| Tue, 16 Aug 2022 17:24:58 +0200 |
blanchet |
revived 'try0' and 'smart' Isar proofs in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 22 Feb 2022 12:45:14 +0100 |
blanchet |
more handling of Zipperposition definitions in Isar proof construction
|
file |
diff |
annotate
|
| Tue, 22 Feb 2022 12:36:01 +0100 |
blanchet |
handle Zipperposition definitions in Isar proof construction
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 17:33:12 +0100 |
blanchet |
robustly handle empty proof blocks in Isar proof output
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 12:32:33 +0100 |
blanchet |
don't perform preplaying steps if preplaying is disabled
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 11:52:40 +0100 |
blanchet |
tuned punctuation
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 10:58:09 +0100 |
blanchet |
guard against duplicate lines in Zipperposition proofs
|
file |
diff |
annotate
|
| Tue, 01 Dec 2020 15:29:54 +0100 |
desharna |
tuned proof preplay to explicitly refer to Z3 backend
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 11:00:34 +0100 |
desharna |
Tuned indentation
|
file |
diff |
annotate
|
| Thu, 22 Oct 2020 15:18:08 +0200 |
desharna |
Tuned isar_step datatype
|
file |
diff |
annotate
|
| Wed, 21 Oct 2020 17:46:51 +0200 |
desharna |
Tuned isar_proofs constructions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2020 17:31:15 +0200 |
desharna |
Tuned isar_proof datatype
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 16:07:41 +0100 |
desharna |
Added smt (verit) to Sledgehammer's proof preplay.
|
file |
diff |
annotate
|
| Wed, 28 Oct 2020 08:41:07 +0100 |
Mathias Fleury |
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Fri, 02 Oct 2020 10:18:50 +0200 |
desharna |
Add more tacing to sledgehammer_isar_trace
|
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 14:14:56 +0200 |
blanchet |
removed experimental encoding for Waldmeister
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 16:24:04 +0100 |
fleury |
add reconstruction by veriT in method smt
|
file |
diff |
annotate
|
| Fri, 20 Jul 2018 22:19:42 +0200 |
blanchet |
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 15:12:57 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|