Tue, 30 Aug 2011 16:07:34 +0200 |
blanchet |
first step towards polymorphic TFF + changed defaults for Vampire
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:29:39 +0200 |
nik |
removed explicit reliance on Hilbert_Choice.Eps
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
improved handling of induction rules in Sledgehammer
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 14:12:55 +0200 |
nik |
added generation of induction rules
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 21:52:11 +0200 |
blanchet |
change default for generation of tag idempotence and tag argument equations
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 10:12:17 +0200 |
blanchet |
comment
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 01:14:49 +0200 |
blanchet |
improve completeness of polymorphic encodings
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 00:19:25 +0200 |
blanchet |
mangle tag bound declarations properly
|
file |
diff |
annotate
|
Fri, 26 Aug 2011 00:05:45 +0200 |
blanchet |
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 23:54:57 +0200 |
blanchet |
honor TFF Implicit
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 23:38:09 +0200 |
blanchet |
make polymorphic encodings more complete
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 22:06:25 +0200 |
blanchet |
make default unsound mode less unsound
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 19:02:47 +0200 |
blanchet |
added config options to control two aspects of the translation, for evaluation purposes
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 13:55:52 +0100 |
nik |
added choice operator output for
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
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 |
blanchet |
fixed bang encoding detection of which types to encode
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 15:25:39 +0200 |
blanchet |
make sure that all facts are passed to ATP from minimizer
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 23:18:13 +0200 |
blanchet |
fixed "hBOOL" of existential variables, and generate more helpers
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
fixed TFF slicing
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 14:44:19 +0200 |
blanchet |
added formats to the slice and use TFF for remote Vampire
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
we must tag any type whose ground types intersect a nonmonotonic type
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
revert guard logic -- make sure that typing information is generated for existentials
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
generate tag equations for existential variables
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning, plus started implementing tag equation generation for existential variables
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
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 |
blanchet |
clearer terminology
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
remove needless typing information
|
file |
diff |
annotate
|
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
|