src/HOL/Tools/ATP/atp_translate.ML
2011-07-17 blanchet 2011-07-17 fixed lambda-liftg: must ensure the formulas are in close form
2011-07-17 blanchet 2011-07-17 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)
2011-07-17 blanchet 2011-07-17 pass kind to lambda-translation function
2011-07-17 blanchet 2011-07-17 more refactoring of preprocessing
2011-07-17 blanchet 2011-07-17 more refactoring of preprocessing, so as to be able to centralize it
2011-07-17 blanchet 2011-07-17 renamed internal data structure
2011-07-17 blanchet 2011-07-17 simplify code -- there are no lambdas in helpers anyway
2011-07-17 blanchet 2011-07-17 added lambda-lifting to Sledgehammer (rough)
2011-07-17 blanchet 2011-07-17 move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
2011-07-14 blanchet 2011-07-14 move error logic closer to user
2011-07-14 blanchet 2011-07-14 move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
2011-07-14 blanchet 2011-07-14 added option to control which lambda translation to use (for experiments)
2011-07-06 blanchet 2011-07-06 make SML/NJ happier
2011-07-06 blanchet 2011-07-06 make SML/NJ happy + tuning
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF
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