| Wed, 11 Jul 2012 21:43:19 +0200 |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file | diff | annotate |
| Wed, 11 Jul 2012 21:43:19 +0200 |
split relevance filter code into three files
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
export useful functions
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
tuning
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
tuning
|
file | diff | annotate |
| Wed, 23 May 2012 21:19:48 +0200 |
tuned names
|
file | diff | annotate |
| Tue, 22 May 2012 16:59:27 +0200 |
added "ext_cong_neq" lemma (not used yet); tuning
|
file | diff | annotate |
| Thu, 17 May 2012 13:36:23 +0200 |
added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)
|
file | diff | annotate |
| Wed, 16 May 2012 18:16:51 +0200 |
treat sets specially in relevance filter, as they used to, to avoid cluttering the problem with facts about Set.member and Collect
|
file | diff | annotate |
| Thu, 10 May 2012 16:56:23 +0200 |
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
|
file | diff | annotate |
| Thu, 26 Apr 2012 00:33:23 +0200 |
tuning
|
file | diff | annotate |
| Tue, 27 Mar 2012 16:59:13 +0300 |
be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)
|
file | diff | annotate |
| Wed, 21 Mar 2012 16:53:24 +0100 |
generate weights and precedences for predicates as well
|
file | diff | annotate |
| Mon, 19 Mar 2012 21:10:33 +0100 |
moved some legacy stuff;
|
file | diff | annotate |
| Sat, 17 Mar 2012 09:51:18 +0100 |
'definition' no longer exports the foundational "raw_def";
|
file | diff | annotate |
| Tue, 28 Feb 2012 15:54:51 +0100 |
speed up Sledgehammer's clasimpset lookup a bit
|
file | diff | annotate |
| Wed, 08 Feb 2012 00:05:22 +0100 |
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
|
file | diff | annotate |
| Thu, 02 Feb 2012 01:55:17 +0100 |
tuning
|
file | diff | annotate |
| Wed, 01 Feb 2012 12:47:43 +0100 |
proper statuses for "fact_from_ref"
|
file | diff | annotate |
| Tue, 31 Jan 2012 12:43:48 +0100 |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
file | diff | annotate |
| Thu, 26 Jan 2012 20:49:54 +0100 |
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
|
file | diff | annotate |
| Thu, 26 Jan 2012 20:49:54 +0100 |
separate orthogonal components
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Sat, 14 Jan 2012 19:06:05 +0100 |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file | diff | annotate |
| Mon, 02 Jan 2012 14:32:20 +0100 |
removed special handling for set constants in relevance filter
|
file | diff | annotate |
| Sat, 24 Dec 2011 16:14:58 +0100 |
dropped references to obsolete facts `mem_def` and `Collect_def`
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
added sorted DFG output for coming version of SPASS
|
file | diff | annotate |
| Wed, 21 Sep 2011 15:55:15 +0200 |
tuned comment
|
file | diff | annotate |
| Thu, 15 Sep 2011 10:57:40 +0200 |
tuning
|
file | diff | annotate |
| Wed, 07 Sep 2011 13:50:17 +0200 |
parse new experimental '@' encodings
|
file | diff | annotate |
| Wed, 07 Sep 2011 13:50:17 +0200 |
tuning
|
file | diff | annotate |
| Wed, 31 Aug 2011 11:52:03 +0200 |
more tuning
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
improved handling of induction rules in Sledgehammer
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
added generation of induction rules
|
file | diff | annotate |
| Wed, 24 Aug 2011 11:17:33 +0200 |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
removed unused configuration option
|
file | diff | annotate |
| Mon, 27 Jun 2011 22:44:44 +0200 |
merged
|
file | diff | annotate |
| Mon, 27 Jun 2011 15:03:55 +0200 |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file | diff | annotate |
| Mon, 27 Jun 2011 14:56:33 +0200 |
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
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:38 +0200 |
insert rather than append special facts to make it less likely that they're truncated away
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
respect "really_all" argument, which is used by "ATP_Export"
|
file | diff | annotate |
| Thu, 16 Jun 2011 13:50:35 +0200 |
fixed soundness bug related to extensionality
|
file | diff | annotate |
| Fri, 10 Jun 2011 12:01:15 +0200 |
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
|
file | diff | annotate |
| Thu, 09 Jun 2011 16:34:49 +0200 |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file | diff | annotate |
| Tue, 07 Jun 2011 14:17:35 +0200 |
optimized the relevance filter a little bit
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
first step in sharing more code between ATP and Metis translation
|
file | diff | annotate |
| Mon, 30 May 2011 17:00:38 +0200 |
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
tuning -- the "appropriate" terminology is inspired from TPTP
|
file | diff | annotate |
| Sun, 22 May 2011 14:51:42 +0200 |
improved Waldmeister support -- even run it by default on unit equational goals
|
file | diff | annotate |
| Tue, 17 May 2011 15:11:36 +0200 |
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
|
file | diff | annotate |
| Sun, 15 May 2011 16:40:24 +0200 |
tuned signature;
|
file | diff | annotate |
| Sat, 14 May 2011 21:42:17 +0200 |
slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
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
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
remove unused parameter
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
no penality for constants that appear in chained facts
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
tune whitespace
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
added configuration options for experimental features
|
file | diff | annotate |