| Wed, 12 Dec 2012 00:24:06 +0100 |
blanchet |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:52:33 +0100 |
wenzelm |
generalized notion of active area, where sendback is just one application;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:51 +0100 |
blanchet |
don't have MaSh pretend it knows facts it doesn't know
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
fixed embarrassing off-by-one bug in MaSh's Mesh
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
tweak MaSh fudge factors
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 17:48:04 +0100 |
blanchet |
use proper entry point for MaSh in test driver
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 15:54:17 +0100 |
blanchet |
parse more liberal MaSh suggestion syntax (for the eval driver)
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
tweaked MaSh proximity
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
reduce max number of dependencies for MaSh to get rid of junk
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
more feature tweaks
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
prioritize chained facts
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
more MaSh feature tweaking
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
record free variables as a MaSh feature
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
expand type classes into their ancestors for MaSh
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
tweaked MaSh features, based on comments by Josef Urban
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
increase weight of local facts again (MaSh)
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 11:25:10 +0100 |
blanchet |
simplify code now that "mash.py" supports weights
|
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
|
| Wed, 05 Dec 2012 10:35:58 +0100 |
blanchet |
tweaked order of theorems to avoid forward dependencies (MaSh)
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:43:24 +0100 |
blanchet |
more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:19:03 +0100 |
blanchet |
added feature weights in MaSh
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:19:02 +0100 |
blanchet |
promote local facts using a hack (for MaSh)
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 19:10:14 +0100 |
blanchet |
turned off noisy MaSh features
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 10:02:51 +0100 |
blanchet |
simplify MaSh term patterns + add missing global facts if there aren't too many
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 00:37:11 +0100 |
blanchet |
MaSh improvements: deeper patterns + more respect for chained facts
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 23:43:53 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 20:55:34 +0100 |
blanchet |
proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 13:24:55 +0100 |
blanchet |
robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
|
file |
diff |
annotate
|