| 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
|
| Thu, 21 Apr 2011 22:18:28 +0200 |
blanchet |
detect some unsound proofs before showing them to the user
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:31:48 +0100 |
blanchet |
give more weight to Frees than to Consts in relevance filter
|
file |
diff |
annotate
|
| Thu, 17 Feb 2011 12:14:47 +0100 |
blanchet |
export more functionality of Sledgehammer to applications (for experiments)
|
file |
diff |
annotate
|
| Wed, 16 Feb 2011 19:07:53 +0100 |
blanchet |
export useful function (needed in a Sledgehammer-related experiment)
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 13:25:18 +0100 |
blanchet |
escape backticks in altstrings
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:46:54 +0100 |
blanchet |
no need to do a super-duper atomization if Metis fails afterwards anyway
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
reintroduce the higher penalty for skolems
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
comment tuning
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
make it more likely that induction rules are picked up by Sledgehammer
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
instantiate induction rules automatically
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 16:42:06 +0100 |
blanchet |
move facts supplied with "add:" to the front, so that they get a better weight (SMT)
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 12:08:41 +0100 |
blanchet |
honor "overlord" option for SMT solvers as well and don't pass "ext" to them
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
make Sledgehammer's relevance filter include the "ext" rule when appropriate
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 16:27:07 +0100 |
blanchet |
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
|
file |
diff |
annotate
|
| Mon, 08 Nov 2010 02:32:27 +0100 |
blanchet |
better detection of completely irrelevant facts
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 10:25:08 +0100 |
blanchet |
always honor the max relevant constraint
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 09:49:03 +0100 |
blanchet |
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 15:31:26 +0100 |
blanchet |
pass proper type to SMT_Builtin.is_builtin
|
file |
diff |
annotate
|