Wed, 11 Sep 2013 22:20:45 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 22:20:45 +0200 |
blanchet |
get rid of another complication in relevance filter
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 22:20:43 +0200 |
blanchet |
renamed config option
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 18:38:23 +0200 |
blanchet |
kick out totally hopeless facts after 5 iterations to speed things up
|
file |
diff |
annotate
|
Wed, 11 Sep 2013 09:51:19 +0200 |
blanchet |
got rid of currently unused data structure, to speed up relevance filter
|
file |
diff |
annotate
|
Mon, 09 Sep 2013 23:55:35 +0200 |
blanchet |
make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
|
file |
diff |
annotate
|
Fri, 23 Aug 2013 16:14:26 +0200 |
blanchet |
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
|
file |
diff |
annotate
|
Wed, 21 Aug 2013 14:54:25 +0200 |
blanchet |
weight MaSh constants by frequency
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
tuned indent
|
file |
diff |
annotate
|
Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
Sat, 19 Jan 2013 17:42:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 20 Dec 2012 15:51:27 +0100 |
blanchet |
better weight functions for MePo/MaSh etc.
|
file |
diff |
annotate
|
Wed, 05 Dec 2012 13:25:06 +0100 |
blanchet |
take proximity into account for MaSh + fix a debilitating bug in feature generation
|
file |
diff |
annotate
|
Wed, 05 Dec 2012 13:25:06 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 12 Nov 2012 14:46:42 +0100 |
blanchet |
fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:43:51 +0200 |
blanchet |
tune Mesh filter
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML files
|
file |
diff |
annotate
| base
|