| Mon, 27 Jun 2011 14:56:28 +0200 |
added "sound" option to force Sledgehammer to be pedantically sound
|
file | diff | annotate |
| Mon, 27 Jun 2011 13:52:47 +0200 |
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
|
file | diff | annotate |
| Mon, 27 Jun 2011 13:52:47 +0200 |
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:39 +0200 |
order generated facts topologically
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:39 +0200 |
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:39 +0200 |
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
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 |
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 |
use more appropriate type systems for ATP exporter
|
file | diff | annotate |
| Fri, 10 Jun 2011 12:01:15 +0200 |
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 |
compile
|
file | diff | annotate |
| Wed, 08 Jun 2011 15:25:44 +0200 |
modernized Proof_Context;
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
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 |
optimized the relevance filter a little bit
|
file | diff | annotate |
| Tue, 07 Jun 2011 07:06:24 +0200 |
renamed ML function
|
file | diff | annotate |
| Tue, 07 Jun 2011 07:04:53 +0200 |
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
|
file | diff | annotate | base |