src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
2010-08-23 ago perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
2010-08-22 ago don't penalize abstractions in relevance filter + support nameless `foo`-style facts
2010-08-22 ago more work on finite axiom detection
2010-08-20 ago make sure minimizer facts go through "transform_elim_theorems"
2010-08-20 ago unbreak "only" option of Sledgehammer
2010-08-20 ago improve "x = A | x = B | x = C"-style axiom detection
2010-08-20 ago improve "x = A | x = B | x = C"-style fact discovery
2010-08-20 ago transform elim theorems before filtering "bool" and "prop" variables out;
2010-08-20 ago more fiddling with Sledgehammer's "add:" option
2010-08-19 ago generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
2010-08-19 ago 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-18 ago make sure that "add:" doesn't influence the relevance filter too much
2010-08-18 ago tuning of relevance filter
2010-08-18 ago minor cleanup
2010-08-18 ago bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
2010-08-18 ago fix the relevance filter so that it ignores If, Ex1, Ball, Bex
2010-08-12 ago dropped dead code
2010-08-09 ago prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
2010-08-09 ago adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
2010-08-09 ago remove debugging output
2010-07-29 ago handle division by zero gracefully (used to raise Unordered later on)
2010-07-29 ago avoid "_def_raw" theorems
2010-07-29 ago work around atomization failures
2010-07-29 ago fiddle with the fudge factors, to get similar results as before
2010-07-29 ago avoid "clause" and "cnf" terminology where it no longer makes sense
2010-07-27 ago standardize "Author" tags
2010-07-26 ago generate full first-order formulas (FOF) in Sledgehammer
2010-06-29 ago move blacklisting completely out of the clausifier;
2010-06-28 ago always perform relevance filtering on original formulas
2010-06-25 ago got rid of "respect_no_atp" option, which even I don't use
2010-06-25 ago renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 ago merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 ago renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
2010-06-25 ago remove junk
2010-06-25 ago further reduce dependencies on "sledgehammer_fact_filter.ML"
2010-06-25 ago move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
2010-06-25 ago eta-expand
2010-06-25 ago improve the natural formula relevance filter code, so that it behaves more like the CNF one
2010-06-24 ago a76ace919f1c wasn't quite right; second try
2010-06-24 ago make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
2010-06-23 ago improve the new "natural formula" fact filter
2010-06-23 ago fix bug with "skolem_id" + sort facts for increased readability
2010-06-22 ago factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22 ago missing "Unsynchronized" + make exception take a unit
2010-06-22 ago added code to optionally perform fact filtering on the original (non-CNF) formulas
2010-06-22 ago more cosmetics
2010-06-22 ago cosmetics + prevent consideration of inlined Skolem terms in relevance filter
2010-06-22 ago canonical argument order
2010-06-22 ago leverage new data structure for handling "add:" and "del:"
2010-06-22 ago thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
2010-06-22 ago removed Sledgehammer's support for the DFG syntax;
2010-06-21 ago try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-14 ago adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 ago proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-07 ago made SML/NJ happy again;
2010-06-05 ago renaming
2010-06-05 ago show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
2010-06-05 ago make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
2010-06-05 ago totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
2010-05-28 ago make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work