src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
Wed, 21 Sep 2011 15:55:15 +0200 blanchet tuned comment
Thu, 15 Sep 2011 10:57:40 +0200 blanchet tuning
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning
Wed, 31 Aug 2011 11:52:03 +0200 blanchet more tuning
Tue, 30 Aug 2011 14:12:55 +0200 nik improved handling of induction rules in Sledgehammer
Tue, 30 Aug 2011 14:12:55 +0200 nik added generation of induction rules
Wed, 24 Aug 2011 11:17:33 +0200 blanchet more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
Mon, 22 Aug 2011 15:02:45 +0200 blanchet removed unused configuration option
Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged
Mon, 27 Jun 2011 14:56:33 +0200 blanchet don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
Mon, 27 Jun 2011 15:03:55 +0200 wenzelm old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
Tue, 21 Jun 2011 17:17:38 +0200 blanchet insert rather than append special facts to make it less likely that they're truncated away
Mon, 20 Jun 2011 10:41:02 +0200 blanchet respect "really_all" argument, which is used by "ATP_Export"
Thu, 16 Jun 2011 13:50:35 +0200 blanchet fixed soundness bug related to extensionality
Fri, 10 Jun 2011 12:01:15 +0200 blanchet 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
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Tue, 07 Jun 2011 14:17:35 +0200 blanchet optimized the relevance filter a little bit
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Mon, 30 May 2011 17:00:38 +0200 blanchet fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
Tue, 24 May 2011 00:01:33 +0200 blanchet use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
Tue, 24 May 2011 00:01:33 +0200 blanchet tuning -- the "appropriate" terminology is inspired from TPTP
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals
Tue, 17 May 2011 15:11:36 +0200 blanchet append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
Sun, 15 May 2011 16:40:24 +0200 wenzelm tuned signature;
Sat, 14 May 2011 21:42:17 +0200 wenzelm slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
Thu, 12 May 2011 15:29:19 +0200 blanchet 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
Thu, 12 May 2011 15:29:19 +0200 blanchet remove unused parameter
Thu, 12 May 2011 15:29:19 +0200 blanchet fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
Thu, 12 May 2011 15:29:19 +0200 blanchet no penality for constants that appear in chained facts
Thu, 12 May 2011 15:29:19 +0200 blanchet improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
Thu, 12 May 2011 15:29:19 +0200 blanchet tune whitespace
Thu, 12 May 2011 15:29:19 +0200 blanchet added configuration options for experimental features
Thu, 05 May 2011 14:18:58 +0200 blanchet tuning
Wed, 04 May 2011 19:35:48 +0200 blanchet exploit inferred monotonicity
Tue, 03 May 2011 21:46:49 +0200 blanchet fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts
Mon, 02 May 2011 22:52:15 +0200 blanchet recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system
Sun, 01 May 2011 18:37:25 +0200 blanchet 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"
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 16 Apr 2011 13:48:45 +0200 wenzelm Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
Fri, 08 Apr 2011 16:34:14 +0200 wenzelm discontinued special treatment of structure Lexicon;
Fri, 18 Mar 2011 22:55:28 +0100 blanchet added "simp:", "intro:", and "elim:" to "try" command
Thu, 17 Mar 2011 11:18:31 +0100 blanchet add option to relevance filter's "all_facts" function to really get all facts (needed for some experiments)
Mon, 21 Feb 2011 10:31:48 +0100 blanchet give more weight to Frees than to Consts in relevance filter
Thu, 17 Feb 2011 12:14:47 +0100 blanchet export more functionality of Sledgehammer to applications (for experiments)
Wed, 16 Feb 2011 19:07:53 +0100 blanchet export useful function (needed in a Sledgehammer-related experiment)
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString;
Tue, 21 Dec 2010 04:33:17 +0100 blanchet proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
Sun, 19 Dec 2010 13:25:18 +0100 blanchet escape backticks in altstrings
Sat, 18 Dec 2010 21:07:34 +0100 blanchet made the relevance filter treat unatomizable facts like "atomize_all" properly (these result in problems that get E spinning seemingly forever);
Thu, 16 Dec 2010 15:46:54 +0100 blanchet no need to do a super-duper atomization if Metis fails afterwards anyway
Thu, 16 Dec 2010 15:12:17 +0100 blanchet reintroduce the higher penalty for skolems
Thu, 16 Dec 2010 15:12:17 +0100 blanchet comment tuning
Thu, 16 Dec 2010 15:12:17 +0100 blanchet 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
Thu, 16 Dec 2010 15:12:17 +0100 blanchet make it more likely that induction rules are picked up by Sledgehammer
Thu, 16 Dec 2010 15:12:17 +0100 blanchet add the current theory's constant to the goal to make theorems from the current theory more relevant on the first iteration already
less more (0) -60 tip