src/HOL/Tools/ATP/atp_translate.ML
2011-08-25 nik 2011-08-25 added choice operator output for Satallax
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-25 blanchet 2011-08-25 handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
2011-08-25 blanchet 2011-08-25 fixed bang encoding detection of which types to encode
2011-08-24 blanchet 2011-08-24 make sure that all facts are passed to ATP from minimizer
2011-08-24 blanchet 2011-08-24 tuning
2011-08-23 blanchet 2011-08-23 fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23 blanchet 2011-08-23 fixed TFF slicing
2011-08-23 blanchet 2011-08-23 added formats to the slice and use TFF for remote Vampire
2011-08-22 blanchet 2011-08-22 we must tag any type whose ground types intersect a nonmonotonic type
2011-08-22 blanchet 2011-08-22 made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22 blanchet 2011-08-22 revert guard logic -- make sure that typing information is generated for existentials
2011-08-22 blanchet 2011-08-22 generate tag equations for existential variables
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