src/HOL/Tools/ATP/atp_translate.ML
2011-09-07 blanchet 2011-09-07 started work on ghost type arg encoding
2011-09-07 blanchet 2011-09-07 stricted type encoding parsing
2011-09-07 blanchet 2011-09-07 tweaking polymorphic TFF and THF output
2011-09-07 blanchet 2011-09-07 parse new experimental '@' encodings
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed
2011-09-07 blanchet 2011-09-07 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 make mangling sound w.r.t. type arguments
2011-09-07 blanchet 2011-09-07 make "filter_type_args" more robust if the actual arity is higher than the declared one
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
2011-09-06 blanchet 2011-09-06 added dummy polymorphic THF system
2011-09-06 blanchet 2011-09-06 cleanup "simple" type encodings
2011-09-06 blanchet 2011-09-06 drop more type arguments soundly, when they can be deduced from the arg types
2011-09-01 blanchet 2011-09-01 make "sound" sound and "unsound" more sound, based on evaluation
2011-08-31 blanchet 2011-08-31 make SML/NJ happy
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-31 blanchet 2011-08-31 more tuning
2011-08-31 blanchet 2011-08-31 tuning
2011-08-31 blanchet 2011-08-31 avoid relying on dubious TFF1 feature
2011-08-30 blanchet 2011-08-30 generate properly typed TFF1 (PFF) problems in the presence of type class predicates
2011-08-30 blanchet 2011-08-30 added type abstractions (for declaring polymorphic constants) to TFF syntax
2011-08-30 blanchet 2011-08-30 implement more of the polymorphic simply typed format TFF(1)
2011-08-30 blanchet 2011-08-30 extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30 blanchet 2011-08-30 first step towards polymorphic TFF + changed defaults for Vampire
2011-08-30 nik 2011-08-30 removed explicit reliance on Hilbert_Choice.Eps
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-08-30 nik 2011-08-30 added generation of induction rules
2011-08-26 blanchet 2011-08-26 change default for generation of tag idempotence and tag argument equations
2011-08-26 blanchet 2011-08-26 comment
2011-08-26 blanchet 2011-08-26 improve completeness of polymorphic encodings
2011-08-26 blanchet 2011-08-26 mangle tag bound declarations properly
2011-08-26 blanchet 2011-08-26 fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
2011-08-25 blanchet 2011-08-25 honor TFF Implicit
2011-08-25 blanchet 2011-08-25 make polymorphic encodings more complete
2011-08-25 blanchet 2011-08-25 make default unsound mode less unsound
2011-08-25 blanchet 2011-08-25 make TFF output less explicit where possible
2011-08-25 blanchet 2011-08-25 added config options to control two aspects of the translation, for evaluation purposes
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