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