| 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
|