| Thu, 25 Aug 2011 14:25:07 +0200 |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file | diff | annotate |
| Thu, 25 Aug 2011 14:25:07 +0200 |
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
|
file | diff | annotate |
| Thu, 25 Aug 2011 14:25:06 +0200 |
fixed bang encoding detection of which types to encode
|
file | diff | annotate |
| Wed, 24 Aug 2011 15:25:39 +0200 |
make sure that all facts are passed to ATP from minimizer
|
file | diff | annotate |
| Wed, 24 Aug 2011 11:17:33 +0200 |
tuning
|
file | diff | annotate |
| Tue, 23 Aug 2011 23:18:13 +0200 |
fixed "hBOOL" of existential variables, and generate more helpers
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:44:19 +0200 |
fixed TFF slicing
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:44:19 +0200 |
added formats to the slice and use TFF for remote Vampire
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
we must tag any type whose ground types intersect a nonmonotonic type
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
revert guard logic -- make sure that typing information is generated for existentials
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
generate tag equations for existential variables
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
tuning, plus started implementing tag equation generation for existential variables
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
clearer terminology
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
added caching for (in)finiteness checks
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
remove needless typing information
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
cleaner handling of polymorphic monotonicity inference
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
added option to control soundness of encodings more precisely, for evaluation purposes
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
make sound mode more sound (and clean up code)
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
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 |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file | diff | annotate |
| Wed, 10 Aug 2011 20:53:43 +0200 |
old term operations are legacy;
|
file | diff | annotate |
| Tue, 09 Aug 2011 17:33:17 +0200 |
workaround THF parser limitation
|
file | diff | annotate |
| Tue, 09 Aug 2011 09:05:22 +0200 |
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 |
added helpers for "All" and "Ex"
|
file | diff | annotate |
| Thu, 28 Jul 2011 16:32:39 +0200 |
no needless mangling
|
file | diff | annotate |
| Thu, 28 Jul 2011 11:43:45 +0200 |
fixed lambda concealing
|
file | diff | annotate |
| Tue, 26 Jul 2011 22:53:06 +0200 |
renamed "preds" encodings to "guards"
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
further worked around LEO-II parser limitation, with eta-expansion
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
no need for existential witnesses for sorts in TFF and THF formats
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
mangle "undefined"
|
file | diff | annotate |
| Mon, 25 Jul 2011 14:10:12 +0200 |
declare "undefined" constant
|
file | diff | annotate |
| Mon, 25 Jul 2011 14:10:12 +0200 |
avoid needless type args for lifted-lambdas
|
file | diff | annotate |
| Thu, 21 Jul 2011 21:29:10 +0200 |
make "concealed" lambda translation sound
|
file | diff | annotate |
| Wed, 20 Jul 2011 23:47:27 +0200 |
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 |
pass type arguments to lambda-lifted Frees, to account for polymorphism
|
file | diff | annotate |
| Wed, 20 Jul 2011 00:37:42 +0200 |
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 |
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 |
fixed lambda-liftg: must ensure the formulas are in close form
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:12:45 +0200 |
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 |
pass kind to lambda-translation function
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
more refactoring of preprocessing
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
more refactoring of preprocessing, so as to be able to centralize it
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
renamed internal data structure
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
simplify code -- there are no lambdas in helpers anyway
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
added lambda-lifting to Sledgehammer (rough)
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:34 +0200 |
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 |
move error logic closer to user
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
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 |
added option to control which lambda translation to use (for experiments)
|
file | diff | annotate |
| Wed, 06 Jul 2011 17:19:34 +0100 |
make SML/NJ happier
|
file | diff | annotate |
| Wed, 06 Jul 2011 17:19:34 +0100 |
make SML/NJ happy + tuning
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
improved translation of lambdas in THF
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
added generation of lambdas in THF
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
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 |
further repair "mangled_tags", now that tags are also mangled
|
file | diff | annotate |
| Fri, 01 Jul 2011 15:53:38 +0200 |
renamed "type_sys" to "type_enc", which is more accurate
|
file | diff | annotate |
| Fri, 01 Jul 2011 15:53:37 +0200 |
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 |