| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
cleaner handling of polymorphic monotonicity inference
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added option to control soundness of encodings more precisely, for evaluation purposes
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
make sound mode more sound (and clean up code)
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 10:03:58 +0200 |
blanchet |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 17:33:17 +0200 |
blanchet |
workaround THF parser limitation
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 09:05:22 +0200 |
blanchet |
move lambda-lifting code to ATP encoding, so it can be used by Metis
|
file |
diff |
annotate
|
| Thu, 28 Jul 2011 16:32:49 +0200 |
blanchet |
added helpers for "All" and "Ex"
|
file |
diff |
annotate
|
| Thu, 28 Jul 2011 16:32:39 +0200 |
blanchet |
no needless mangling
|
file |
diff |
annotate
|
| Thu, 28 Jul 2011 11:43:45 +0200 |
blanchet |
fixed lambda concealing
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 22:53:06 +0200 |
blanchet |
renamed "preds" encodings to "guards"
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
further worked around LEO-II parser limitation, with eta-expansion
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
no need for existential witnesses for sorts in TFF and THF formats
|
file |
diff |
annotate
|
| Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
mangle "undefined"
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
declare "undefined" constant
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 14:10:12 +0200 |
blanchet |
avoid needless type args for lifted-lambdas
|
file |
diff |
annotate
|
| Thu, 21 Jul 2011 21:29:10 +0200 |
blanchet |
make "concealed" lambda translation sound
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 23:47:27 +0200 |
blanchet |
use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
pass type arguments to lambda-lifted Frees, to account for polymorphism
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 00:37:42 +0200 |
blanchet |
avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:21:19 +0200 |
blanchet |
fixed lambda-liftg: must ensure the formulas are in close form
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:12:45 +0200 |
blanchet |
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
pass kind to lambda-translation function
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
more refactoring of preprocessing
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
more refactoring of preprocessing, so as to be able to centralize it
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
renamed internal data structure
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
simplify code -- there are no lambdas in helpers anyway
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:35 +0200 |
blanchet |
added lambda-lifting to Sledgehammer (rough)
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 14:11:34 +0200 |
blanchet |
move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 17:29:30 +0200 |
blanchet |
move error logic closer to user
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
make SML/NJ happier
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
make SML/NJ happy + tuning
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
improved translation of lambdas in THF
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
added generation of lambdas in THF
|
file |
diff |
annotate
|
| Tue, 05 Jul 2011 17:09:59 +0100 |
nik |
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
further repair "mangled_tags", now that tags are also mangled
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
renamed "type_sys" to "type_enc", which is more accurate
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
mangle "ti" tags
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 14:56:28 +0200 |
blanchet |
added "sound" option to force Sledgehammer to be pedantically sound
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
don't change the way helpers are generated for the exporter's sake
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
avoid double ASCII-fication
|
file |
diff |
annotate
|
| Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
generate type predicates for existentials/skolems, otherwise some problems might not be provable
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
fixed soundness bug related to extensionality
|
file |
diff |
annotate
|
| Wed, 15 Jun 2011 14:36:41 +0200 |
blanchet |
fixed soundness bug made more visible by previous change
|
file |
diff |
annotate
|
| Wed, 15 Jun 2011 14:36:41 +0200 |
blanchet |
type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 00:16:28 +0200 |
blanchet |
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 22:13:49 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 16:20:19 +0200 |
blanchet |
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
|
file |
diff |
annotate
|