| Thu, 09 Jun 2011 16:34:49 +0200 |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file | diff | annotate |
| Thu, 09 Jun 2011 00:16:28 +0200 |
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 |
merged
|
file | diff | annotate |
| Wed, 08 Jun 2011 17:49:01 +0200 |
updated headers;
|
file | diff | annotate |
| Wed, 08 Jun 2011 15:56:57 +0200 |
more robust exception pattern General.Subscript;
|
file | diff | annotate |
| Wed, 08 Jun 2011 16:20:19 +0200 |
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 |
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 |
fixed format selection logic for Waldmeister
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
minor optimization
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
don't needlessly extensionalize
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
don't needlessly presimplify -- makes ATP problem preparation much faster
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
tuned
|
file | diff | annotate |
| Wed, 08 Jun 2011 08:47:43 +0200 |
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 |
slightly faster/cleaner accumulation of polymorphic consts
|
file | diff | annotate |
| Tue, 07 Jun 2011 14:17:35 +0200 |
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
|
file | diff | annotate |
| Tue, 07 Jun 2011 06:58:52 +0200 |
pass props not thms to ATP translator
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:56:06 +0200 |
removed old optimization that isn't one anyone
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:56:06 +0200 |
generate less type information in polymorphic case
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
made "explicit_apply"'s smart mode (more) complete
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
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 |
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 |
whitespace tuning
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
fixed type helper indices in new Metis
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
improved ATP clausifier so it can deal with "x => (y <=> z)"
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
avoid renumbering hypotheses
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
tuning
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
fixed detection of Skolem constants in type construction detection code
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
don't stumble on Skolem names
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
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 |
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 |
properly locate helpers whose constants have several entries in the helper table
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
skip "hBOOL" in new Metis path finder
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:34 +0200 |
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 |
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 |
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 |
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 |
implemented missing hAPP and ti cases of new path finder
|
file | diff | annotate |
| Wed, 01 Jun 2011 10:29:43 +0200 |
support lightweight tags in new Metis
|
file | diff | annotate |
| Wed, 01 Jun 2011 10:29:43 +0200 |
tuned names
|
file | diff | annotate |
| Wed, 01 Jun 2011 10:29:43 +0200 |
distinguish different kinds of typing informations in the fact name
|
file | diff | annotate |
| Wed, 01 Jun 2011 00:23:16 +0200 |
make SML/NJ happier
|
file | diff | annotate |
| Wed, 01 Jun 2011 00:12:38 +0200 |
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 |
no need for type arguments with "xxx_tags_heavy" type system
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
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 |
tuned name
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
make "prepare_atp_problem" more robust w.r.t. choice of type system
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
proper handling of type variable classes in new Metis
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
don't preprocess twice
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
tuning
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
more work on new metis that exploits the powerful new type encodings
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
tuning
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
first step in sharing more code between ATP and Metis translation
|
file | diff | annotate | base |