src/HOL/Tools/ATP/atp_proof.ML
Tue, 24 Nov 2020 19:49:59 +0100 desharna proper parsing of TSTP HOL lines
Thu, 05 Nov 2020 18:14:02 +0100 desharna Added support for TFX to Sledgehammer
Thu, 08 Oct 2020 17:55:17 +0200 blanchet removed support for obsolete prover SNARK and underperforming prover E-Par
Thu, 08 Oct 2020 16:36:00 +0200 desharna drop obsolete ad hoc support for Satallax isar proof reconstruction
Thu, 08 Oct 2020 16:07:10 +0200 desharna recognize THF proofs properly
Fri, 02 Oct 2020 10:18:50 +0200 desharna Add more tacing to sledgehammer_isar_trace
Fri, 25 Oct 2019 15:32:41 +0200 blanchet folded experimental Ehoh into E now that E 2.3 has been released
Fri, 25 Oct 2019 15:23:14 +0200 blanchet removed support for old system E-MaLeS
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
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)
Fri, 25 Oct 2019 14:51:16 +0200 blanchet removed support for iProver-Eq
Fri, 25 Oct 2019 14:14:56 +0200 blanchet removed experimental encoding for Waldmeister
Wed, 09 Oct 2019 18:48:15 +0200 blanchet generalized parsing, for e.g. Leo-III
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Tue, 22 May 2018 17:15:02 +0200 blanchet added lambda-free HO output for Ehoh (higher-order E prototype)
Tue, 07 Nov 2017 15:16:42 +0100 blanchet more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
Tue, 07 Nov 2017 15:16:41 +0100 blanchet integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
Tue, 29 Aug 2017 13:56:15 +0200 blanchet tuned messages
Tue, 29 Aug 2017 13:56:14 +0200 blanchet improved Vampire proof parser
Tue, 15 Aug 2017 15:28:25 +0200 blanchet extended TSTP type parser + tuned messages
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
Mon, 05 Oct 2015 21:46:48 +0200 blanchet added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
Thu, 27 Aug 2015 20:16:07 +0200 blanchet robust handling of Vampire 4 proofs
Tue, 03 Mar 2015 16:37:45 +0100 blanchet SPASS-Pirate is now called Pirate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sun, 12 Oct 2014 21:52:45 +0200 blanchet special treatment of extensionality in minimizer
Mon, 06 Oct 2014 19:19:16 +0200 blanchet get rid of 'individual' type in DFG proofs
Mon, 29 Sep 2014 10:39:39 +0200 blanchet parse back type of SPASS proof variables
Fri, 12 Sep 2014 13:27:32 +0200 fleury correction in the thf0 parser ("(=)" found in a Satallax proof).
Thu, 28 Aug 2014 23:48:46 +0200 blanchet reworked unskolemization for SPASS
Thu, 28 Aug 2014 16:58:27 +0200 blanchet tuned message
Mon, 04 Aug 2014 16:55:03 +0200 blanchet tuned comments
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions
Wed, 30 Jul 2014 14:03:58 +0200 fleury Improving robustness and indentation corrections.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer
Mon, 28 Jul 2014 10:57:33 +0200 blanchet correctly translate THF functions from terms to types
Thu, 24 Jul 2014 18:46:38 +0200 blanchet filter out 'theory(...)' from dependencies early on
Tue, 24 Jun 2014 08:19:57 +0200 blanchet added 'dummy_thf_ml' prover for experiments with HOLyHammer
Mon, 16 Jun 2014 19:41:42 +0200 blanchet fixed parsing of one-argument 'file()' in TSTP files
Mon, 16 Jun 2014 19:39:41 +0200 blanchet give Z3 TPTP proofs a chance
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side
Mon, 16 Jun 2014 16:21:39 +0200 fleury Correcting the type parser
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II.
Wed, 11 Jun 2014 15:29:23 +0200 blanchet moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
Tue, 10 Jun 2014 19:15:14 +0200 blanchet tuning
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover
Tue, 20 May 2014 16:11:37 +0200 blanchet tuning
Fri, 04 Apr 2014 15:56:40 +0200 blanchet use Z3 TPTP cores rather than proofs since the latter are somewhat broken
Fri, 04 Apr 2014 11:49:47 +0200 blanchet improved parsing of "z3_tptp" proofs
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
Fri, 20 Dec 2013 14:27:07 +0100 blanchet recognize datatype reasoning in SPASS-Pirate
Thu, 19 Dec 2013 15:47:17 +0100 blanchet extended ATP types with sorts
Wed, 18 Dec 2013 22:55:20 +0100 blanchet parse SPASS-Pirate types
Wed, 18 Dec 2013 17:00:14 +0100 blanchet fixed variable confusion introduced by 'tuning' change 565f9af86d67
Wed, 18 Dec 2013 16:50:14 +0100 blanchet tuning
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
less more (0) -100 -60 tip