| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 Jan 2012 14:12:20 +0100 |
blanchet |
killed unfold_set_const option that makes no sense now that set is a type constructor again
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
killed "guard@?" encodings -- they were found to be unsound
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
extend previous optimizations to guard-based encodings
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
treat polymorphic constructors specially in @? encodings
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 18:59:50 +0100 |
blanchet |
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 18:59:46 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 13:04:46 +0100 |
blanchet |
ensure TPTP FOF/TFF/THF formulas are close
|
file |
diff |
annotate
|
| Wed, 14 Dec 2011 18:07:32 +0100 |
blanchet |
make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
avoid multiple type decls in TFF (improves on cef82dc1462d)
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
added missing quantifier
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
remove needless declaration in TFF1 problems
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
avoid multiple TFF1 declarations
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated TFF1 support
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
move eta-contraction to before translation to Metis, to ensure everything stays in sync
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
fixed bugs in lambda-lifting code -- ensure distinct names for variables
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
protect prefix against variant mutations
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't pass "lam_lifted" option to "metis" unless there's a good reason
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed needless baggage
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 10:34:08 +0100 |
blanchet |
document "lam_trans" option
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:20:58 +0100 |
blanchet |
rename the lambda translation schemes, so that they are understandable out of context
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
use consts, not frees, for lambda-lifting
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 08:56:23 +0100 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 11:13:47 +0100 |
blanchet |
repaired quantification over type variables for non-TFF1/THF encodings
|
file |
diff |
annotate
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improve handling of bound type variables (esp. for TFF1)
|
file |
diff |
annotate
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improved TFF1 output
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
check "sound" flag before doing something unsound...
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 16:36:13 +0200 |
blanchet |
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:40:59 +0200 |
blanchet |
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:40:58 +0200 |
blanchet |
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 14:30:57 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Thu, 08 Sep 2011 09:25:55 +0200 |
blanchet |
fixed computation of "in_conj" for polymorphic encodings
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
also implemented ghost version of the tagged encodings
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
smarter explicit apply business
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
started work on ghost type arg encoding
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
stricted type encoding parsing
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tweaking polymorphic TFF and THF output
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
parse new experimental '@' encodings
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:50:16 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make mangling sound w.r.t. type arguments
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
make "filter_type_args" more robust if the actual arity is higher than the declared one
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:10:41 +0200 |
blanchet |
rationalize uniform encodings
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 18:13:36 +0200 |
blanchet |
added dummy polymorphic THF system
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 11:31:01 +0200 |
blanchet |
cleanup "simple" type encodings
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
drop more type arguments soundly, when they can be deduced from the arg types
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 13:18:27 +0200 |
blanchet |
make "sound" sound and "unsound" more sound, based on evaluation
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 13:22:50 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:52:03 +0200 |
blanchet |
more tuning
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:23:16 +0200 |
blanchet |
more tuning
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:14:53 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 11:12:27 +0200 |
blanchet |
avoid relying on dubious TFF1 feature
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added type abstractions (for declaring polymorphic constants) to TFF syntax
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
implement more of the polymorphic simply typed format TFF(1)
|
file |
diff |
annotate
|
| Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
extended simple types with polymorphism -- the implementation still needs some work though
|
file |
diff |
annotate
|
| 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
|