src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-24 blanchet 2010-08-24 clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name
2010-08-24 blanchet 2010-08-24 quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
2010-08-19 blanchet 2010-08-19 parse SNARK proofs
2010-08-19 blanchet 2010-08-19 no spurious trailing "\n" at the end of Sledgehammer's output
2010-08-17 blanchet 2010-08-17 tuning
2010-08-17 blanchet 2010-08-17 handle E's Skolem constants more gracefully
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-07-30 blanchet 2010-07-30 don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...
2010-07-29 blanchet 2010-07-29 avoid "clause" and "cnf" terminology where it no longer makes sense
2010-07-29 blanchet 2010-07-29 kill polymorphic "val"s
2010-07-28 blanchet 2010-07-28 fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
2010-07-28 blanchet 2010-07-28 revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well; we can no longer just count the formulas, because for some reason E's numbering either no longer starts at 1 or it doesn't increment by 1 at each step
2010-07-28 blanchet 2010-07-28 more robust proof reconstruction
2010-07-28 blanchet 2010-07-28 fix remote_vampire's proof reconstruction
2010-07-28 blanchet 2010-07-28 fix proof reconstruction for latest Vampire
2010-07-28 blanchet 2010-07-28 renaming
2010-07-28 blanchet 2010-07-28 support latest version of Vampire (1.0) locally
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 standardize "Author" tags
2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-07-27 blanchet 2010-07-27 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
2010-07-27 blanchet 2010-07-27 implemented "sublinear" minimization algorithm
2010-07-27 blanchet 2010-07-27 extract sort constraints from FOFs properly; we can't rely on having them as separate literals anymore
2010-07-27 blanchet 2010-07-27 handle Vampire's equality proxy axiom correctly
2010-07-26 blanchet 2010-07-26 remove more Skolemization-aware code
2010-07-26 blanchet 2010-07-26 simplify "conjecture_shape" business, as a result of using FOF instead of CNF
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-07-26 blanchet 2010-07-26 proof reconstruction for full FOF terms
2010-07-23 blanchet 2010-07-23 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.
2010-07-23 blanchet 2010-07-23 first step in using "fof" rather than "cnf" in TPTP problems
2010-07-21 blanchet 2010-07-21 renamings + only need second component of name pool to reconstruct proofs
2010-06-30 blanchet 2010-06-30 rewrote the TPTP problem generation code more or less from scratch; there is now an explicit AST data structure which will make it easy to support alternative formats (e.g., DFG, sorted TPTP, sorted DFG); also, if "full_types" is enabled, "hAPP" is then tagged properly
2010-06-29 blanchet 2010-06-29 move "nice names" from Metis to TPTP format
2010-06-28 blanchet 2010-06-28 always perform relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
2010-06-25 blanchet 2010-06-25 merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
2010-06-25 blanchet 2010-06-25 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; the new name reflects that it's not used only by Sledgehammer (but also by "meson" and "metis") and that it doesn't only clausify facts (but also goals)
2010-06-25 blanchet 2010-06-25 more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
2010-06-22 blanchet 2010-06-22 removed Sledgehammer's support for the DFG syntax; this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
2010-06-21 blanchet 2010-06-21 try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
2010-06-14 blanchet 2010-06-14 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
2010-06-11 blanchet 2010-06-11 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
2010-06-04 blanchet 2010-06-04 fix bugs in Sledgehammer's Isar proof "redirection" code
2010-06-02 blanchet 2010-06-02 handle Vampire's definitions smoothly
2010-06-02 blanchet 2010-06-02 fix bug in direct Isar proofs, which was exhibited by the "BigO" example
2010-06-02 blanchet 2010-06-02 show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously
2010-05-28 blanchet 2010-05-28 merged
2010-05-28 blanchet 2010-05-28 make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-17 blanchet 2010-05-17 make sure chained facts don't pop up in the metis proof
2010-05-17 blanchet 2010-05-17 fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
2010-05-14 blanchet 2010-05-14 renamed options
2010-05-14 blanchet 2010-05-14 made Sledgehammer's full-typed proof reconstruction work for the first time; previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code
2010-05-01 krauss 2010-05-01 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-05-01 krauss 2010-05-01 Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
2010-05-01 blanchet 2010-05-01 now if this doesn't make SML/NJ happy, nothing will
2010-04-30 blanchet 2010-04-30 eliminate trivial case splits from Isar proofs