src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
Thu, 26 Aug 2010 09:23:21 +0200 blanchet add a bonus for chained facts, since they are likely to be relevant;
Thu, 26 Aug 2010 01:03:08 +0200 blanchet add a penalty for lambda-abstractions;
Thu, 26 Aug 2010 00:49:04 +0200 blanchet fiddle with relevance filter
Wed, 25 Aug 2010 19:41:18 +0200 blanchet reorganize options regarding to the relevance threshold and decay
Wed, 25 Aug 2010 17:49:52 +0200 blanchet make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
Wed, 25 Aug 2010 09:42:28 +0200 blanchet simplify more code
Wed, 25 Aug 2010 09:34:28 +0200 blanchet cosmetics
Wed, 25 Aug 2010 09:32:43 +0200 blanchet get rid of "defs_relevant" feature;
Wed, 25 Aug 2010 09:02:07 +0200 blanchet renamed "relevance_convergence" to "relevance_decay"
Tue, 24 Aug 2010 22:57:22 +0200 blanchet make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
Tue, 24 Aug 2010 19:19:28 +0200 blanchet compute names lazily;
Tue, 24 Aug 2010 18:03:43 +0200 blanchet clean handling of whether a fact is chained or not;
Tue, 24 Aug 2010 16:43:52 +0200 blanchet don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
Tue, 24 Aug 2010 16:24:11 +0200 blanchet quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
Tue, 24 Aug 2010 15:07:54 +0200 blanchet cosmetics
Mon, 23 Aug 2010 23:32:11 +0200 blanchet cosmetics
Mon, 23 Aug 2010 23:24:24 +0200 blanchet optimize fact filter some more
Mon, 23 Aug 2010 23:00:57 +0200 blanchet cache previous iteration's weights, and keep track of what's dirty and what's clean;
Mon, 23 Aug 2010 21:55:52 +0200 blanchet modified relevance filter
Mon, 23 Aug 2010 18:53:11 +0200 blanchet invert semantics of "relevance_convergence", to make it more intuitive
Mon, 23 Aug 2010 18:39:12 +0200 blanchet if no facts were selected on first iteration, try again with a lower threshold
Mon, 23 Aug 2010 18:25:49 +0200 blanchet weed out junk in relevance filter
Mon, 23 Aug 2010 18:04:31 +0200 blanchet no need for "eq" facts -- good old "=" is good enough for us
Mon, 23 Aug 2010 17:49:18 +0200 blanchet destroy elim rules before checking for finite exhaustive facts
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
Sun, 22 Aug 2010 16:56:05 +0200 blanchet don't penalize abstractions in relevance filter + support nameless `foo`-style facts
Sun, 22 Aug 2010 08:26:09 +0200 blanchet more work on finite axiom detection
Fri, 20 Aug 2010 17:52:26 +0200 blanchet make sure minimizer facts go through "transform_elim_theorems"
Fri, 20 Aug 2010 16:44:48 +0200 blanchet unbreak "only" option of Sledgehammer
Fri, 20 Aug 2010 16:22:51 +0200 blanchet improve "x = A | x = B | x = C"-style axiom detection
Fri, 20 Aug 2010 14:15:29 +0200 blanchet improve "x = A | x = B | x = C"-style fact discovery
Fri, 20 Aug 2010 14:09:02 +0200 blanchet transform elim theorems before filtering "bool" and "prop" variables out;
Fri, 20 Aug 2010 13:39:47 +0200 blanchet more fiddling with Sledgehammer's "add:" option
Thu, 19 Aug 2010 19:34:11 +0200 blanchet generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
Thu, 19 Aug 2010 18:16:47 +0200 blanchet 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
Wed, 18 Aug 2010 20:17:03 +0200 blanchet make sure that "add:" doesn't influence the relevance filter too much
Wed, 18 Aug 2010 19:57:12 +0200 blanchet tuning of relevance filter
Wed, 18 Aug 2010 18:01:54 +0200 blanchet minor cleanup
Wed, 18 Aug 2010 17:53:12 +0200 blanchet bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
Wed, 18 Aug 2010 16:39:05 +0200 blanchet fix the relevance filter so that it ignores If, Ex1, Ball, Bex
Thu, 12 Aug 2010 17:56:44 +0200 haftmann dropped dead code
Mon, 09 Aug 2010 14:08:30 +0200 blanchet prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
Mon, 09 Aug 2010 14:00:32 +0200 blanchet adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
Mon, 09 Aug 2010 10:39:53 +0200 blanchet remove debugging output
Thu, 29 Jul 2010 22:57:36 +0200 blanchet handle division by zero gracefully (used to raise Unordered later on)
Thu, 29 Jul 2010 19:58:43 +0200 blanchet avoid "_def_raw" theorems
Thu, 29 Jul 2010 17:45:22 +0200 blanchet work around atomization failures
Thu, 29 Jul 2010 16:54:46 +0200 blanchet fiddle with the fudge factors, to get similar results as before
Thu, 29 Jul 2010 14:53:55 +0200 blanchet avoid "clause" and "cnf" terminology where it no longer makes sense
Tue, 27 Jul 2010 19:17:15 +0200 blanchet standardize "Author" tags
Mon, 26 Jul 2010 17:03:21 +0200 blanchet generate full first-order formulas (FOF) in Sledgehammer
Tue, 29 Jun 2010 10:25:53 +0200 blanchet move blacklisting completely out of the clausifier;
Mon, 28 Jun 2010 17:31:38 +0200 blanchet always perform relevance filtering on original formulas
Fri, 25 Jun 2010 17:26:14 +0200 blanchet got rid of "respect_no_atp" option, which even I don't use
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
Fri, 25 Jun 2010 15:16:22 +0200 blanchet remove junk
Fri, 25 Jun 2010 15:08:03 +0200 blanchet further reduce dependencies on "sledgehammer_fact_filter.ML"
Fri, 25 Jun 2010 15:01:35 +0200 blanchet move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
less more (0) -100 -60 tip