src/HOL/Tools/ATP/atp_translate.ML
2011-08-22 blanchet 2011-08-22 tuning, plus started implementing tag equation generation for existential variables
2011-08-22 blanchet 2011-08-22 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
2011-08-22 blanchet 2011-08-22 clearer terminology
2011-08-22 blanchet 2011-08-22 added caching for (in)finiteness checks
2011-08-22 blanchet 2011-08-22 remove needless typing information
2011-08-22 blanchet 2011-08-22 cleaner handling of polymorphic monotonicity inference
2011-08-22 blanchet 2011-08-22 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-22 blanchet 2011-08-22 added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22 blanchet 2011-08-22 make sound mode more sound (and clean up code)
2011-08-22 blanchet 2011-08-22 reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-08-17 blanchet 2011-08-17 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-09 blanchet 2011-08-09 workaround THF parser limitation
2011-08-09 blanchet 2011-08-09 move lambda-lifting code to ATP encoding, so it can be used by Metis
2011-07-28 blanchet 2011-07-28 added helpers for "All" and "Ex"
2011-07-28 blanchet 2011-07-28 no needless mangling
2011-07-28 blanchet 2011-07-28 fixed lambda concealing
2011-07-26 blanchet 2011-07-26 renamed "preds" encodings to "guards"
2011-07-26 blanchet 2011-07-26 further worked around LEO-II parser limitation, with eta-expansion
2011-07-26 blanchet 2011-07-26 no need for existential witnesses for sorts in TFF and THF formats
2011-07-26 blanchet 2011-07-26 mangle "undefined"
2011-07-25 blanchet 2011-07-25 declare "undefined" constant
2011-07-25 blanchet 2011-07-25 avoid needless type args for lifted-lambdas
2011-07-21 blanchet 2011-07-21 make "concealed" lambda translation sound
2011-07-20 blanchet 2011-07-20 use a more robust naming convention for "polymorphic" frees -- the check is an overapproximation but that's fine as far as soundness is concerned
2011-07-20 blanchet 2011-07-20 pass type arguments to lambda-lifted Frees, to account for polymorphism
2011-07-20 blanchet 2011-07-20 generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
2011-07-20 blanchet 2011-07-20 avoid calling "Term.is_first_order" (indirectly) on a term with loose de Bruijns -- this is not necessary anyway because of the Abs check in "simple_translate_lambdas"
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