| Wed, 16 May 2012 18:16:51 +0200 |
blanchet |
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 |
blanchet |
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 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 16:59:13 +0300 |
blanchet |
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 |
blanchet |
generate weights and precedences for predicates as well
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 09:51:18 +0100 |
wenzelm |
'definition' no longer exports the foundational "raw_def";
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 15:54:51 +0100 |
blanchet |
speed up Sledgehammer's clasimpset lookup a bit
|
file |
diff |
annotate
|
| Wed, 08 Feb 2012 00:05:22 +0100 |
blanchet |
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 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 01 Feb 2012 12:47:43 +0100 |
blanchet |
proper statuses for "fact_from_ref"
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 12:43:48 +0100 |
blanchet |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
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 |
blanchet |
separate orthogonal components
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 14:32:20 +0100 |
blanchet |
removed special handling for set constants in relevance filter
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 16:14:58 +0100 |
haftmann |
dropped references to obsolete facts `mem_def` and `Collect_def`
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Wed, 21 Sep 2011 15:55:15 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Thu, 15 Sep 2011 10:57:40 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
parse new experimental '@' encodings
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:52:03 +0200 |
blanchet |
more tuning
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
removed unused configuration option
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 22:44:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
respect "really_all" argument, which is used by "ATP_Export"
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
fixed soundness bug related to extensionality
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
optimized the relevance filter a little bit
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
tuning -- the "appropriate" terminology is inspired from TPTP
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
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 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 21:42:17 +0200 |
wenzelm |
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 |
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
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
remove unused parameter
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
no penality for constants that appear in chained facts
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
tune whitespace
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added configuration options for experimental features
|
file |
diff |
annotate
|
| Thu, 05 May 2011 14:18:58 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 04 May 2011 19:35:48 +0200 |
blanchet |
exploit inferred monotonicity
|
file |
diff |
annotate
|
| Tue, 03 May 2011 21:46:49 +0200 |
blanchet |
fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
|
file |
diff |
annotate
|
| Tue, 03 May 2011 00:10:22 +0200 |
blanchet |
replaced some Unsynchronized.refs with Config.Ts
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
have each ATP filter out dangerous facts for themselves, based on their type system
|
file |
diff |
annotate
|
| 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"
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
implement the new ATP type system in Sledgehammer
|
file |
diff |
annotate
|