| 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
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
fixed format selection logic for Waldmeister
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 17:49:01 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:56:57 +0200 |
wenzelm |
more robust exception pattern General.Subscript;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
minor optimization
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly extensionalize
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
tuned
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:47:43 +0200 |
blanchet |
slightly faster/cleaner accumulation of polymorphic consts
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 14:17:35 +0200 |
blanchet |
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 06:58:52 +0200 |
blanchet |
pass props not thms to ATP translator
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
removed old optimization that isn't one anyone
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:56:06 +0200 |
blanchet |
generate less type information in polymorphic case
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
made "explicit_apply"'s smart mode (more) complete
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
change var name as a workaround for rare issue in Metis's reconstruction code -- namely, "find_var" fails because "X = X" is wrongly mirrorred as "A = A"
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed type helper indices in new Metis
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
improved ATP clausifier so it can deal with "x => (y <=> z)"
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
avoid renumbering hypotheses
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
fixed detection of Skolem constants in type construction detection code
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't stumble on Skolem names
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
don't merge "hAPP"s even in unsound heavy modes, because "hAPP" then sometimes gets declared with too strict arguments ("ind"), and we lose some proofs
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
properly locate helpers whose constants have several entries in the helper table
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
skip "hBOOL" in new Metis path finder
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
|
file |
diff |
annotate
|
| Mon, 06 Jun 2011 20:36:34 +0200 |
blanchet |
added support for helpers in new Metis, so far only for polymorphic type encodings
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 19:50:59 +0200 |
blanchet |
fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
implemented missing hAPP and ti cases of new path finder
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
support lightweight tags in new Metis
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 10:29:43 +0200 |
blanchet |
distinguish different kinds of typing informations in the fact name
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 00:23:16 +0200 |
blanchet |
make SML/NJ happier
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 00:12:38 +0200 |
blanchet |
make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
no need for type arguments with "xxx_tags_heavy" type system
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
use ":" for type information (looks good in Metis's output) and handle it in new path finder
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuned name
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
make "prepare_atp_problem" more robust w.r.t. choice of type system
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
proper handling of type variable classes in new Metis
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
don't preprocess twice
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
| base
|