| Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
|
file |
diff |
annotate
|
| Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
|
file |
diff |
annotate
|
| Wed, 15 Jun 2011 14:36:41 +0200 |
blanchet |
use more appropriate type systems for ATP exporter
|
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 00:16:28 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:25:44 +0200 |
wenzelm |
modernized Proof_Context;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
optimized the relevance filter a little bit
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:06:24 +0200 |
blanchet |
renamed ML function
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 07:04:53 +0200 |
blanchet |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
file |
diff |
annotate
| base
|