| 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
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
file |
diff |
annotate
|
| Mon, 28 Jul 2014 10:57:33 +0200 |
blanchet |
correctly translate THF functions from terms to types
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 18:46:38 +0200 |
blanchet |
filter out 'theory(...)' from dependencies early on
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 08:19:57 +0200 |
blanchet |
added 'dummy_thf_ml' prover for experiments with HOLyHammer
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:41:42 +0200 |
blanchet |
fixed parsing of one-argument 'file()' in TSTP files
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:39:41 +0200 |
blanchet |
give Z3 TPTP proofs a chance
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:21:52 +0200 |
fleury |
Moving the remote prefix deleting on Sledgehammer's side
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:21:39 +0200 |
fleury |
Correcting the type parser
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:18:34 +0200 |
fleury |
imported patch leo2_skolem_simplication
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 16:18:15 +0200 |
fleury |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 15:29:23 +0200 |
blanchet |
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 19:15:14 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Tue, 20 May 2014 16:11:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 15:56:40 +0200 |
blanchet |
use Z3 TPTP cores rather than proofs since the latter are somewhat broken
|
file |
diff |
annotate
|
| Fri, 04 Apr 2014 11:49:47 +0200 |
blanchet |
improved parsing of "z3_tptp" proofs
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 20:39:49 +0100 |
blanchet |
unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
|
file |
diff |
annotate
|