Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
Mon, 23 Aug 2010 17:49:18 +0200 blanchet destroy elim rules before checking for finite exhaustive facts file | diff | annotate
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; file | diff | annotate
Sun, 22 Aug 2010 16:56:05 +0200 blanchet don't penalize abstractions in relevance filter + support nameless `foo`-style facts file | diff | annotate
Sun, 22 Aug 2010 08:26:09 +0200 blanchet more work on finite axiom detection file | diff | annotate
Fri, 20 Aug 2010 17:52:26 +0200 blanchet make sure minimizer facts go through "transform_elim_theorems" file | diff | annotate
Fri, 20 Aug 2010 16:44:48 +0200 blanchet unbreak "only" option of Sledgehammer file | diff | annotate
Fri, 20 Aug 2010 16:22:51 +0200 blanchet improve "x = A | x = B | x = C"-style axiom detection file | diff | annotate
Fri, 20 Aug 2010 14:15:29 +0200 blanchet improve "x = A | x = B | x = C"-style fact discovery file | diff | annotate
Fri, 20 Aug 2010 14:09:02 +0200 blanchet transform elim theorems before filtering "bool" and "prop" variables out; file | diff | annotate
Fri, 20 Aug 2010 13:39:47 +0200 blanchet more fiddling with Sledgehammer's "add:" option file | diff | annotate
Thu, 19 Aug 2010 19:34:11 +0200 blanchet generalize the "too general equality" code to handle facts like "x ~= A ==> x = B" file | diff | annotate
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 file | diff | annotate
Wed, 18 Aug 2010 20:17:03 +0200 blanchet make sure that "add:" doesn't influence the relevance filter too much file | diff | annotate
Wed, 18 Aug 2010 19:57:12 +0200 blanchet tuning of relevance filter file | diff | annotate
Wed, 18 Aug 2010 18:01:54 +0200 blanchet minor cleanup file | diff | annotate
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") file | diff | annotate
Wed, 18 Aug 2010 16:39:05 +0200 blanchet fix the relevance filter so that it ignores If, Ex1, Ball, Bex file | diff | annotate
Thu, 12 Aug 2010 17:56:44 +0200 haftmann dropped dead code file | diff | annotate
Mon, 09 Aug 2010 14:08:30 +0200 blanchet prevent ATP thread for staying around for 1 minute if an exception occurred earlier; file | diff | annotate
Mon, 09 Aug 2010 14:00:32 +0200 blanchet adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present file | diff | annotate
Mon, 09 Aug 2010 10:39:53 +0200 blanchet remove debugging output file | diff | annotate
Thu, 29 Jul 2010 22:57:36 +0200 blanchet handle division by zero gracefully (used to raise Unordered later on) file | diff | annotate
Thu, 29 Jul 2010 19:58:43 +0200 blanchet avoid "_def_raw" theorems file | diff | annotate
Thu, 29 Jul 2010 17:45:22 +0200 blanchet work around atomization failures file | diff | annotate
Thu, 29 Jul 2010 16:54:46 +0200 blanchet fiddle with the fudge factors, to get similar results as before file | diff | annotate
Thu, 29 Jul 2010 14:53:55 +0200 blanchet avoid "clause" and "cnf" terminology where it no longer makes sense file | diff | annotate
Tue, 27 Jul 2010 19:17:15 +0200 blanchet standardize "Author" tags file | diff | annotate
Mon, 26 Jul 2010 17:03:21 +0200 blanchet generate full first-order formulas (FOF) in Sledgehammer file | diff | annotate
Tue, 29 Jun 2010 10:25:53 +0200 blanchet move blacklisting completely out of the clausifier; file | diff | annotate
Mon, 28 Jun 2010 17:31:38 +0200 blanchet always perform relevance filtering on original formulas file | diff | annotate
Fri, 25 Jun 2010 17:26:14 +0200 blanchet got rid of "respect_no_atp" option, which even I don't use file | diff | annotate
Fri, 25 Jun 2010 17:08:39 +0200 blanchet renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer file | diff | annotate
Fri, 25 Jun 2010 16:42:06 +0200 blanchet merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME file | diff | annotate
Fri, 25 Jun 2010 16:15:03 +0200 blanchet renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; file | diff | annotate
Fri, 25 Jun 2010 15:16:22 +0200 blanchet remove junk file | diff | annotate
Fri, 25 Jun 2010 15:08:03 +0200 blanchet further reduce dependencies on "sledgehammer_fact_filter.ML" file | diff | annotate
Fri, 25 Jun 2010 15:01:35 +0200 blanchet move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML"; file | diff | annotate
Fri, 25 Jun 2010 12:15:24 +0200 blanchet eta-expand file | diff | annotate
Fri, 25 Jun 2010 12:08:48 +0200 blanchet improve the natural formula relevance filter code, so that it behaves more like the CNF one file | diff | annotate
Thu, 24 Jun 2010 18:22:15 +0200 blanchet a76ace919f1c wasn't quite right; second try file | diff | annotate
Thu, 24 Jun 2010 10:38:01 +0200 blanchet make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds file | diff | annotate
Wed, 23 Jun 2010 18:43:50 +0200 blanchet improve the new "natural formula" fact filter file | diff | annotate
Wed, 23 Jun 2010 12:43:09 +0200 blanchet fix bug with "skolem_id" + sort facts for increased readability file | diff | annotate
Tue, 22 Jun 2010 23:54:02 +0200 blanchet factor out TPTP format output into file of its own, to facilitate further changes file | diff | annotate
Tue, 22 Jun 2010 18:47:45 +0200 blanchet missing "Unsynchronized" + make exception take a unit file | diff | annotate
Tue, 22 Jun 2010 18:31:49 +0200 blanchet added code to optionally perform fact filtering on the original (non-CNF) formulas file | diff | annotate
Tue, 22 Jun 2010 17:10:01 +0200 blanchet more cosmetics file | diff | annotate
Tue, 22 Jun 2010 17:07:39 +0200 blanchet cosmetics + prevent consideration of inlined Skolem terms in relevance filter file | diff | annotate
Tue, 22 Jun 2010 16:50:55 +0200 blanchet canonical argument order file | diff | annotate
Tue, 22 Jun 2010 16:40:36 +0200 blanchet leverage new data structure for handling "add:" and "del:" file | diff | annotate
Tue, 22 Jun 2010 16:23:29 +0200 blanchet thread original theorem along with CNF theorem, as a step toward killing the Skolem cache file | diff | annotate
Tue, 22 Jun 2010 14:28:22 +0200 blanchet removed Sledgehammer's support for the DFG syntax; file | diff | annotate
Mon, 21 Jun 2010 12:31:41 +0200 blanchet try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better file | diff | annotate
Mon, 14 Jun 2010 10:36:01 +0200 blanchet adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" file | diff | annotate
Fri, 11 Jun 2010 17:10:23 +0200 blanchet proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter file | diff | annotate
Mon, 07 Jun 2010 17:13:36 +0200 wenzelm made SML/NJ happy again; file | diff | annotate
Sat, 05 Jun 2010 21:30:40 +0200 blanchet renaming file | diff | annotate
Sat, 05 Jun 2010 16:39:23 +0200 blanchet 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 file | diff | annotate
Sat, 05 Jun 2010 15:59:58 +0200 blanchet make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases; file | diff | annotate
Sat, 05 Jun 2010 15:07:50 +0200 blanchet totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax; file | diff | annotate
less more (0) -60 tip
isabelle