| 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
|