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"
2010-06-24 blanchet 2010-06-24 make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
2010-06-23 blanchet 2010-06-23 have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
2010-06-22 blanchet 2010-06-22 factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-21 blanchet 2010-06-21 try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-14 blanchet 2010-06-14 A function called "untyped_aconv" shouldn't look at the bound names!
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-12 blanchet 2010-06-12 "raise Fail" for internal errors + one new internal error (instead of "Match")
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-02 blanchet 2010-06-02 give more helpful error message
2010-05-17 blanchet 2010-05-17 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-17 blanchet 2010-05-17 generate proper arity declarations for TFrees for SPASS's DFG format; and renamed a confusing function in the process
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-04-29 blanchet 2010-04-29 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)
2010-04-26 blanchet 2010-04-26 adapt code to reflect new signature of "neg_clausify"
2010-04-24 blanchet 2010-04-24 better error reporting; in particular, users shouldn't panic if "metis" can prove "False", especially in "neg_clausify"-style proofs
2010-04-19 blanchet 2010-04-19 added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
2010-04-16 blanchet 2010-04-16 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
2010-04-16 blanchet 2010-04-16 store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-15 blanchet 2010-04-15 give more sensible names to "fol_type" constructors, as requested by a FIXME comment
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;