| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
avoid detour through terms
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
cleanly distinguish between type declarations and symbol declarations
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
removed old hack now that types and terms are cleanly distinguished in the data structure
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
added sorts to datastructure
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
robustness -- TFF1 does not support type classes
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
implement polymorphic DFG output, without type classes for now
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 17:50:06 +0200 |
blanchet |
sound monotonicity inference in the presence of "aggressive" helpers
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 17:50:06 +0200 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
prevent an "Empty" exception (e.g. with Satallax, "mono_native")
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
added "args_query" encodings
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
killed most unsound encodings
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
generalized monotonic constructor optimisation so that it works with e.g. the product type
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
removed micro-optimization whose justification I can't recall
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
more aggressive type argument optimization
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
use cover for "poly_guards" encoding
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
hack to make LEO-II perform better on TPTP THF problems
|
file |
diff |
annotate
|
| Wed, 06 Jun 2012 10:35:05 +0200 |
blanchet |
don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway
|
file |
diff |
annotate
|
| Mon, 28 May 2012 20:45:28 +0200 |
blanchet |
killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
|
file |
diff |
annotate
|
| Mon, 28 May 2012 20:25:38 +0200 |
blanchet |
don't generate definitions for LEO-II -- this cuases more harm than good
|
file |
diff |
annotate
|
| Thu, 24 May 2012 18:21:54 +0200 |
blanchet |
make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
|
file |
diff |
annotate
|
| Thu, 24 May 2012 15:01:29 +0200 |
blanchet |
gracefully handle definition-looking premises
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy)
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
generate THF definitions
|
file |
diff |
annotate
|
| Wed, 23 May 2012 12:02:27 +0200 |
wenzelm |
merged, abandoning change of src/HOL/Tools/ATP/atp_problem_generate.ML from 6ea205a4d7fd;
|
file |
diff |
annotate
|
| Tue, 22 May 2012 16:59:27 +0200 |
blanchet |
make higher-order goals more first-order via extensionality
|
file |
diff |
annotate
|