| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
reverted 0506c3273814 -- the message is still useful
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
more robust E proof parsing
|
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 17:01:42 +0100 |
blanchet |
removed rarely used error in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 22 Feb 2022 12:36:01 +0100 |
blanchet |
handle Zipperposition definitions in Isar proof construction
|
file |
diff |
annotate
|
| Tue, 22 Feb 2022 09:58:25 +0100 |
blanchet |
parse Zipperposition definitions
|
file |
diff |
annotate
|
| Mon, 14 Feb 2022 16:34:56 +0100 |
blanchet |
print Sledgehammer error message
|
file |
diff |
annotate
|
| Mon, 07 Feb 2022 16:59:37 +0100 |
blanchet |
more robust TSTP proof parsing
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 18:12:04 +0100 |
blanchet |
made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 16:16:50 +0100 |
blanchet |
correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives
|
file |
diff |
annotate
|
| Tue, 01 Feb 2022 12:14:43 +0100 |
blanchet |
adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs
|
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 |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 17:14:21 +0200 |
desharna |
tuned TPTP parsing of THF function application
|
file |
diff |
annotate
|
| Fri, 27 Aug 2021 14:29:02 +0200 |
blanchet |
handle Zipperposition's ResourceOut gracefully
|
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:53 +0200 |
blanchet |
parse TPTP operator @ also when not parenthesized
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 15:42:52 +0200 |
blanchet |
removed support for experimental Pirate prover
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 16:30:17 +0200 |
blanchet |
parse logical operators in the right order w.r.t. backtracking
|
file |
diff |
annotate
|
| Mon, 12 Jul 2021 16:30:16 +0200 |
blanchet |
improved warning
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 21:02:34 +0100 |
wenzelm |
removed spurious references to perl / libwww-perl;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2020 15:31:31 +0100 |
desharna |
tweaked tptp parsing when source info is missing
|
file |
diff |
annotate
|
| Tue, 24 Nov 2020 19:49:59 +0100 |
desharna |
proper parsing of TSTP HOL lines
|
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 16:36:00 +0200 |
desharna |
drop obsolete ad hoc support for Satallax isar proof reconstruction
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 16:07:10 +0200 |
desharna |
recognize THF proofs properly
|
file |
diff |
annotate
|
| Fri, 02 Oct 2020 10:18:50 +0200 |
desharna |
Add more tacing to sledgehammer_isar_trace
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 15:32:41 +0200 |
blanchet |
folded experimental Ehoh into E now that E 2.3 has been released
|
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 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:14:56 +0200 |
blanchet |
removed experimental encoding for Waldmeister
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 18:48:15 +0200 |
blanchet |
generalized parsing, for e.g. Leo-III
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
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:42 +0100 |
blanchet |
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
|
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
|
| Tue, 29 Aug 2017 13:56:15 +0200 |
blanchet |
tuned messages
|
file |
diff |
annotate
|
| Tue, 29 Aug 2017 13:56:14 +0200 |
blanchet |
improved Vampire proof parser
|
file |
diff |
annotate
|
| Tue, 15 Aug 2017 15:28:25 +0200 |
blanchet |
extended TSTP type parser + tuned messages
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 21:46:48 +0200 |
blanchet |
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 20:16:07 +0200 |
blanchet |
robust handling of Vampire 4 proofs
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
special treatment of extensionality in minimizer
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 19:19:16 +0200 |
blanchet |
get rid of 'individual' type in DFG proofs
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
parse back type of SPASS proof variables
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 13:27:32 +0200 |
fleury |
correction in the thf0 parser ("(=)" found in a Satallax proof).
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:48:46 +0200 |
blanchet |
reworked unskolemization for SPASS
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 16:55:03 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 16:53:09 +0200 |
blanchet |
deal with E definitions
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:58 +0200 |
fleury |
Improving robustness and indentation corrections.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch hilbert_choice_support
|
file |
diff |
annotate
|