src/HOL/Tools/Sledgehammer/metis_tactics.ML
2010-09-27 blanchet 2010-09-27 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-20 blanchet 2010-09-20 revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
2010-09-20 blanchet 2010-09-20 preprocess "Ex" before doing clausification in Metis; this is dual to "All" in b96941dddd04
2010-09-20 blanchet 2010-09-20 merge tracing of two related modules
2010-09-18 blanchet 2010-09-18 preprocess "All" before doing clausification in Metis; helps the definitional clausifier produce fewer clauses
2010-09-16 blanchet 2010-09-16 complete refactoring of Metis along the lines of Sledgehammer
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16 blanchet 2010-09-16 supply the Metis parameter defaults as argument, instead of patching the Metis sources; these values were found by Larry in 2007 and using anything else risks losing proofs
2010-09-15 blanchet 2010-09-15 "Metis." -> "Metis_" to reflect change in "metis.ML"
2010-09-14 blanchet 2010-09-14 tuning
2010-09-14 blanchet 2010-09-14 tuning
2010-09-13 blanchet 2010-09-13 adapt to latest Metis version
2010-09-09 blanchet 2010-09-09 use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
2010-09-09 blanchet 2010-09-09 clarify comment
2010-09-09 blanchet 2010-09-09 improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs
2010-09-09 blanchet 2010-09-09 add cutoff beyond which facts are handled using definitional CNF
2010-09-08 blanchet 2010-09-08 workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer; to reproduce the old bug, replace the command by(rule new_Addr_SomeD) on line 27 of Jinja/J/TypeSafe.thy with by (metis new_Addr_SomeD)
2010-09-03 blanchet 2010-09-03 remove code I submitted accidentally
2010-09-03 blanchet 2010-09-03 disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method
2010-09-02 blanchet 2010-09-02 FIXME -> TODO (nothing is broken)
2010-09-02 blanchet 2010-09-02 Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
2010-09-01 blanchet 2010-09-01 fiddled with fudge factor (based on Mirabelle)
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-26 blanchet 2010-08-26 renaming
2010-08-24 blanchet 2010-08-24 revert this idea of automatically invoking "metisFT" when "metis" fails; there are very few good reasons why "metisFT" should succeed when "metis" fails, and "metisFT" tends to "diverge" more often than "metis -- furthermore the exception handling code wasn't working properly
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-22 blanchet 2010-08-22 treat "using X by metis" (more or less) the same as "by (metis X)"
2010-08-20 blanchet 2010-08-20 temporarily disable "fequal" handling in Metis; one proof fails in "HOL-Auth" because of the new rules
2010-08-20 blanchet 2010-08-20 merged
2010-08-19 blanchet 2010-08-19 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
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-08-16 blanchet 2010-08-16 Geoff's formatter now needs closed formulas
2010-08-09 blanchet 2010-08-09 replace recursion with "fold"
2010-07-29 blanchet 2010-07-29 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses
2010-07-29 blanchet 2010-07-29 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
2010-07-29 blanchet 2010-07-29 revert exception throwing in FOL_SOLVE, since they're not caught anyway
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 standardize "Author" tags
2010-07-27 blanchet 2010-07-27 get rid of more dead wood
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-07-26 blanchet 2010-07-26 renamed internal function
2010-07-21 blanchet 2010-07-21 revert code that was submitted by mistake
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-07-21 blanchet 2010-07-21 rename "classrel" to "class_rel"
2010-07-21 blanchet 2010-07-21 rename "combtyp" constructors
2010-07-21 blanchet 2010-07-21 renamed "Literal" to "FOLLiteral"
2010-06-30 blanchet 2010-06-30 rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly
2010-06-29 blanchet 2010-06-29 move function
2010-06-29 blanchet 2010-06-29 Sledgehammer can save some msecs by cheating
2010-06-29 blanchet 2010-06-29 move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache
2010-06-29 blanchet 2010-06-29 rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
2010-06-29 blanchet 2010-06-29 move functions not needed by Metis out of "Metis_Clauses"
2010-06-28 blanchet 2010-06-28 killed "expand_defs_tac"; it has no raison d'etre now that Skolemization is always done "inline"; the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-25 blanchet 2010-06-25 fewer dependencies
2010-06-25 blanchet 2010-06-25 more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
2010-06-25 blanchet 2010-06-25 move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; since it has nothing to do with filtering
2010-06-24 blanchet 2010-06-24 make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"