src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 blanchet 2010-08-27 merged
2010-08-27 blanchet 2010-08-27 turn off experimental feature per default + avoid exception on "theory constant"
2010-08-27 blanchet 2010-08-27 extended relevance filter with first-order term matching
2010-08-27 blanchet 2010-08-27 rename and simplify
2010-08-27 blanchet 2010-08-27 cosmetics
2010-08-27 blanchet 2010-08-27 renaming + treat "TFree" better in "pattern_for_type"
2010-08-27 blanchet 2010-08-27 fix threshold computation + remove "op =" from relevant constants
2010-08-26 blanchet 2010-08-26 avoid needless "that" fact
2010-08-26 blanchet 2010-08-26 add nameless chained facts to the pool of things known to Sledgehammer
2010-08-26 blanchet 2010-08-26 if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
2010-08-26 blanchet 2010-08-26 improve SPASS hack, when a clause comes from several facts
2010-08-26 blanchet 2010-08-26 lower penalty for Skolem constants
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-26 blanchet 2010-08-26 add a bonus for chained facts, since they are likely to be relevant; (especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible
2010-08-26 blanchet 2010-08-26 add a penalty for lambda-abstractions; the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic; lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply
2010-08-26 blanchet 2010-08-26 fiddle with relevance filter
2010-08-25 blanchet 2010-08-25 reorganize options regarding to the relevance threshold and decay
2010-08-25 blanchet 2010-08-25 make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)
2010-08-25 blanchet 2010-08-25 simplify more code
2010-08-25 blanchet 2010-08-25 cosmetics
2010-08-25 blanchet 2010-08-25 get rid of "defs_relevant" feature; nobody uses it and it works poorly
2010-08-25 blanchet 2010-08-25 renamed "relevance_convergence" to "relevance_decay"
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-24 blanchet 2010-08-24 compute names lazily; there's no point to compute the names of 10000 facts when only 500 are used
2010-08-24 blanchet 2010-08-24 clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name
2010-08-24 blanchet 2010-08-24 don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
2010-08-24 blanchet 2010-08-24 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
2010-08-24 blanchet 2010-08-24 cosmetics
2010-08-23 blanchet 2010-08-23 cosmetics
2010-08-23 blanchet 2010-08-23 optimize fact filter some more
2010-08-23 blanchet 2010-08-23 cache previous iteration's weights, and keep track of what's dirty and what's clean; this speeds up the relevance filter significantly
2010-08-23 blanchet 2010-08-23 modified relevance filter
2010-08-23 blanchet 2010-08-23 invert semantics of "relevance_convergence", to make it more intuitive
2010-08-23 blanchet 2010-08-23 if no facts were selected on first iteration, try again with a lower threshold
2010-08-23 blanchet 2010-08-23 weed out junk in relevance filter
2010-08-23 blanchet 2010-08-23 no need for "eq" facts -- good old "=" is good enough for us
2010-08-23 blanchet 2010-08-23 destroy elim rules before checking for finite exhaustive facts
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 don't penalize abstractions in relevance filter + support nameless `foo`-style facts
2010-08-22 blanchet 2010-08-22 more work on finite axiom detection
2010-08-20 blanchet 2010-08-20 make sure minimizer facts go through "transform_elim_theorems"
2010-08-20 blanchet 2010-08-20 unbreak "only" option of Sledgehammer
2010-08-20 blanchet 2010-08-20 improve "x = A | x = B | x = C"-style axiom detection
2010-08-20 blanchet 2010-08-20 improve "x = A | x = B | x = C"-style fact discovery
2010-08-20 blanchet 2010-08-20 transform elim theorems before filtering "bool" and "prop" variables out; another consequence of the transition to FOF
2010-08-20 blanchet 2010-08-20 more fiddling with Sledgehammer's "add:" option
2010-08-19 blanchet 2010-08-19 generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
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-18 blanchet 2010-08-18 make sure that "add:" doesn't influence the relevance filter too much
2010-08-18 blanchet 2010-08-18 tuning of relevance filter
2010-08-18 blanchet 2010-08-18 minor cleanup
2010-08-18 blanchet 2010-08-18 bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
2010-08-18 blanchet 2010-08-18 fix the relevance filter so that it ignores If, Ex1, Ball, Bex
2010-08-12 haftmann 2010-08-12 dropped dead code
2010-08-09 blanchet 2010-08-09 prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch
2010-08-09 blanchet 2010-08-09 adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
2010-08-09 blanchet 2010-08-09 remove debugging output