src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
2011-06-27 wenzelm 2011-06-27 old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-21 blanchet 2011-06-21 insert rather than append special facts to make it less likely that they're truncated away
2011-06-20 blanchet 2011-06-20 respect "really_all" argument, which is used by "ATP_Export"
2011-06-16 blanchet 2011-06-16 fixed soundness bug related to extensionality
2011-06-10 blanchet 2011-06-10 compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-07 blanchet 2011-06-07 optimized the relevance filter a little bit
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-05-30 blanchet 2011-05-30 fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
2011-05-24 blanchet 2011-05-24 use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
2011-05-24 blanchet 2011-05-24 tuning -- the "appropriate" terminology is inspired from TPTP
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-17 blanchet 2011-05-17 append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
2011-05-15 wenzelm 2011-05-15 tuned signature;
2011-05-14 wenzelm 2011-05-14 slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
2011-05-12 blanchet 2011-05-12 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
2011-05-12 blanchet 2011-05-12 remove unused parameter
2011-05-12 blanchet 2011-05-12 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
2011-05-12 blanchet 2011-05-12 no penality for constants that appear in chained facts
2011-05-12 blanchet 2011-05-12 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
2011-05-12 blanchet 2011-05-12 tune whitespace
2011-05-12 blanchet 2011-05-12 added configuration options for experimental features
2011-05-05 blanchet 2011-05-05 tuning
2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-05-03 blanchet 2011-05-03 fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet 2011-05-02 recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
2011-05-02 blanchet 2011-05-02 have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-03-18 blanchet 2011-03-18 added "simp:", "intro:", and "elim:" to "try" command
2011-03-17 blanchet 2011-03-17 add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter
2011-02-17 blanchet 2011-02-17 export more functionality of Sledgehammer to applications (for experiments)
2011-02-16 blanchet 2011-02-16 export useful function (needed in a Sledgehammer-related experiment)
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-21 blanchet 2010-12-21 proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction
2010-12-19 blanchet 2010-12-19 escape backticks in altstrings
2010-12-18 blanchet 2010-12-18 made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever); disabled inductions (E and SPASS don't like them), but kept "ext" (seems more harmless)
2010-12-16 blanchet 2010-12-16 no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 blanchet 2010-12-16 reintroduce the higher penalty for skolems
2010-12-16 blanchet 2010-12-16 comment tuning
2010-12-16 blanchet 2010-12-16 get rid of experimental feature of term patterns in relevance filter -- doesn't work well unless we take into consideration the equality theory entailed by the relevant facts
2010-12-16 blanchet 2010-12-16 make it more likely that induction rules are picked up by Sledgehammer
2010-12-16 blanchet 2010-12-16 add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
2010-12-16 blanchet 2010-12-16 instantiate induction rules automatically
2010-12-15 blanchet 2010-12-15 move facts supplied with "add:" to the front, so that they get a better weight (SMT)
2010-12-15 blanchet 2010-12-15 honor "overlord" option for SMT solvers as well and don't pass "ext" to them
2010-12-15 blanchet 2010-12-15 make Sledgehammer's relevance filter include the "ext" rule when appropriate
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-07 blanchet 2010-12-07 pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
2010-11-08 blanchet 2010-11-08 better detection of completely irrelevant facts
2010-11-06 blanchet 2010-11-06 always honor the max relevant constraint
2010-11-05 blanchet 2010-11-05 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-04 blanchet 2010-11-04 pass proper type to SMT_Builtin.is_builtin