2011-07-05 nik 2011-07-05 added generation of lambdas in THF
2011-07-05 nik 2011-07-05 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
2011-07-01 blanchet 2011-07-01 further repair "mangled_tags", now that tags are also mangled
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate
2011-07-01 blanchet 2011-07-01 cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
2011-07-01 blanchet 2011-07-01 mangle "ti" tags
2011-07-01 blanchet 2011-07-01 tuning
2011-06-27 blanchet 2011-06-27 added "sound" option to force Sledgehammer to be pedantically sound
2011-06-21 blanchet 2011-06-21 don't change the way helpers are generated for the exporter's sake
2011-06-21 blanchet 2011-06-21 remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
2011-06-21 blanchet 2011-06-21 avoid double ASCII-fication
2011-06-21 blanchet 2011-06-21 generate type predicates for existentials/skolems, otherwise some problems might not be provable
2011-06-16 blanchet 2011-06-16 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"
2011-06-16 blanchet 2011-06-16 fixed soundness bug related to extensionality
2011-06-15 blanchet 2011-06-15 fixed soundness bug made more visible by previous change
2011-06-15 blanchet 2011-06-15 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
2011-06-10 blanchet 2011-06-10 name tuning
2011-06-10 blanchet 2011-06-10 revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09 blanchet 2011-06-09 cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-08 wenzelm 2011-06-08 merged
2011-06-08 blanchet 2011-06-08 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
2011-06-08 blanchet 2011-06-08 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
2011-06-08 blanchet 2011-06-08 fixed format selection logic for Waldmeister
2011-06-08 wenzelm 2011-06-08 updated headers;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-06-08 blanchet 2011-06-08 minor optimization
2011-06-08 blanchet 2011-06-08 don't needlessly extensionalize
2011-06-08 blanchet 2011-06-08 don't needlessly presimplify -- makes ATP problem preparation much faster
2011-06-08 blanchet 2011-06-08 tuned
2011-06-08 blanchet 2011-06-08 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-08 blanchet 2011-06-08 slightly faster/cleaner accumulation of polymorphic consts
2011-06-07 blanchet 2011-06-07 more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
2011-06-07 blanchet 2011-06-07 pass props not thms to ATP translator
2011-06-06 blanchet 2011-06-06 removed old optimization that isn't one anyone
2011-06-06 blanchet 2011-06-06 generate less type information in polymorphic case
2011-06-06 blanchet 2011-06-06 made "explicit_apply"'s smart mode (more) complete
2011-06-06 blanchet 2011-06-06 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"
2011-06-06 blanchet 2011-06-06 make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s
2011-06-06 blanchet 2011-06-06 whitespace tuning
2011-06-06 blanchet 2011-06-06 fixed type helper indices in new Metis
2011-06-06 blanchet 2011-06-06 improved ATP clausifier so it can deal with "x => (y <=> z)"
2011-06-06 blanchet 2011-06-06 avoid renumbering hypotheses
2011-06-06 blanchet 2011-06-06 tuning
2011-06-06 blanchet 2011-06-06 fixed detection of Skolem constants in type construction detection code
2011-06-06 blanchet 2011-06-06 also exploit type tag idempotence in lightweight encodings, following a suggestion from Gothenburg
2011-06-06 blanchet 2011-06-06 don't stumble on Skolem names
2011-06-06 blanchet 2011-06-06 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
2011-06-06 blanchet 2011-06-06 use "" type only in THF and TFF -- might cause strange failures if used in FOF or CNF, depending on how liberal the prover is
2011-06-06 blanchet 2011-06-06 properly locate helpers whose constants have several entries in the helper table
2011-06-06 blanchet 2011-06-06 skip "hBOOL" in new Metis path finder
2011-06-06 blanchet 2011-06-06 ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)
2011-06-06 blanchet 2011-06-06 added support for helpers in new Metis, so far only for polymorphic type encodings
2011-06-01 blanchet 2011-06-01 fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2
2011-06-01 blanchet 2011-06-01 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
2011-06-01 blanchet 2011-06-01 implemented missing hAPP and ti cases of new path finder
2011-06-01 blanchet 2011-06-01 support lightweight tags in new Metis
2011-06-01 blanchet 2011-06-01 tuned names
2011-06-01 blanchet 2011-06-01 distinguish different kinds of typing informations in the fact name
2011-06-01 blanchet 2011-06-01 make SML/NJ happier