src/HOL/Tools/Sledgehammer/metis_tactics.ML
Thu, 02 Sep 2010 13:45:23 +0200 blanchet FIXME -> TODO (nothing is broken)
Thu, 02 Sep 2010 13:18:19 +0200 blanchet Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
Wed, 01 Sep 2010 11:59:04 +0200 blanchet fiddled with fudge factor (based on Mirabelle)
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Thu, 26 Aug 2010 00:49:38 +0200 blanchet renaming
Tue, 24 Aug 2010 15:29:13 +0200 blanchet revert this idea of automatically invoking "metisFT" when "metis" fails;
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
Sun, 22 Aug 2010 14:27:30 +0200 blanchet treat "using X by metis" (more or less) the same as "by (metis X)"
Fri, 20 Aug 2010 15:56:00 +0200 blanchet temporarily disable "fequal" handling in Metis;
Fri, 20 Aug 2010 14:18:55 +0200 blanchet merged
Thu, 19 Aug 2010 18:16:47 +0200 blanchet encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Mon, 16 Aug 2010 09:39:05 +0200 blanchet Geoff's formatter now needs closed formulas
Mon, 09 Aug 2010 11:03:54 +0200 blanchet replace recursion with "fold"
Thu, 29 Jul 2010 22:43:46 +0200 blanchet use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
Thu, 29 Jul 2010 22:13:15 +0200 blanchet fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
Thu, 29 Jul 2010 20:15:50 +0200 blanchet revert exception throwing in FOL_SOLVE, since they're not caught anyway
Tue, 27 Jul 2010 19:41:19 +0200 blanchet minor refactoring
Tue, 27 Jul 2010 19:17:15 +0200 blanchet standardize "Author" tags
Tue, 27 Jul 2010 17:15:12 +0200 blanchet get rid of more dead wood
Mon, 26 Jul 2010 14:14:24 +0200 blanchet make TPTP generator accept full first-order formulas
Mon, 26 Jul 2010 11:21:25 +0200 blanchet renamed internal function
Wed, 21 Jul 2010 21:15:49 +0200 blanchet revert code that was submitted by mistake
Wed, 21 Jul 2010 21:15:07 +0200 blanchet renamings + only need second component of name pool to reconstruct proofs
Wed, 21 Jul 2010 21:14:47 +0200 blanchet rename "classrel" to "class_rel"
Wed, 21 Jul 2010 21:14:26 +0200 blanchet rename "combtyp" constructors
Wed, 21 Jul 2010 21:14:07 +0200 blanchet renamed "Literal" to "FOLLiteral"
Wed, 30 Jun 2010 18:03:34 +0200 blanchet rewrote the TPTP problem generation code more or less from scratch;
Tue, 29 Jun 2010 11:29:31 +0200 blanchet move function
Tue, 29 Jun 2010 10:56:45 +0200 blanchet Sledgehammer can save some msecs by cheating
Tue, 29 Jun 2010 10:25:53 +0200 blanchet move blacklisting completely out of the clausifier;
Tue, 29 Jun 2010 09:26:56 +0200 blanchet rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
Tue, 29 Jun 2010 09:05:37 +0200 blanchet move functions not needed by Metis out of "Metis_Clauses"
Mon, 28 Jun 2010 18:08:36 +0200 blanchet killed "expand_defs_tac";
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
Fri, 25 Jun 2010 16:03:34 +0200 blanchet fewer dependencies
Fri, 25 Jun 2010 15:59:13 +0200 blanchet more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
Fri, 25 Jun 2010 15:01:35 +0200 blanchet move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
Thu, 24 Jun 2010 21:00:37 +0200 blanchet make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
Thu, 24 Jun 2010 10:38:01 +0200 blanchet make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
Wed, 23 Jun 2010 14:36:23 +0200 blanchet have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
Tue, 22 Jun 2010 23:54:02 +0200 blanchet factor out TPTP format output into file of its own, to facilitate further changes
Tue, 22 Jun 2010 14:28:22 +0200 blanchet removed Sledgehammer's support for the DFG syntax;
Mon, 21 Jun 2010 12:31:41 +0200 blanchet try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
Mon, 14 Jun 2010 20:16:36 +0200 blanchet A function called "untyped_aconv" shouldn't look at the bound names!
Mon, 14 Jun 2010 10:36:01 +0200 blanchet adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
Sat, 12 Jun 2010 11:11:07 +0200 blanchet "raise Fail" for internal errors + one new internal error (instead of "Match")
Fri, 11 Jun 2010 17:10:23 +0200 blanchet proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
Wed, 02 Jun 2010 12:28:42 +0200 blanchet give more helpful error message
Mon, 17 May 2010 12:15:37 +0200 blanchet fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
Mon, 17 May 2010 10:18:14 +0200 blanchet generate proper arity declarations for TFrees for SPASS's DFG format;
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Fri, 14 May 2010 11:23:42 +0200 blanchet made Sledgehammer's full-typed proof reconstruction work for the first time;
Thu, 29 Apr 2010 10:25:26 +0200 blanchet use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
Mon, 26 Apr 2010 21:18:20 +0200 blanchet adapt code to reflect new signature of "neg_clausify"
Sat, 24 Apr 2010 16:05:42 +0200 blanchet better error reporting;
Mon, 19 Apr 2010 18:14:45 +0200 blanchet added warning about inconsistent context to Metis;
Fri, 16 Apr 2010 15:49:13 +0200 blanchet added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
less more (0) -60 tip