src/HOL/Tools/ATP/atp_translate.ML
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
2011-06-01 blanchet 2011-06-01 make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
2011-05-31 blanchet 2011-05-31 no need for type arguments with "xxx_tags_heavy" type system
2011-05-31 blanchet 2011-05-31 use ":" for type information (looks good in Metis's output) and handle it in new path finder
2011-05-31 blanchet 2011-05-31 tuned name
2011-05-31 blanchet 2011-05-31 make "prepare_atp_problem" more robust w.r.t. choice of type system
2011-05-31 blanchet 2011-05-31 proper handling of type variable classes in new Metis
2011-05-31 blanchet 2011-05-31 don't preprocess twice
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 more work on new metis that exploits the powerful new type encodings
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation