src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
2010-09-27 blanchet 2010-09-27 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
2010-09-16 blanchet 2010-09-16 factored out TSTP/SPASS/Vampire proof parsing; from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
2010-09-14 blanchet 2010-09-14 use same hack as in "Async_Manager" to work around Proof General bug
2010-09-01 blanchet 2010-09-01 minor refactoring
2010-09-01 blanchet 2010-09-01 translate the axioms to FOF once and for all ATPs
2010-09-01 blanchet 2010-09-01 run relevance filter in a thread, to avoid blocking
2010-08-30 blanchet 2010-08-30 merged
2010-08-30 blanchet 2010-08-30 bring Sledgehammer's combinators in line with Metis's; cf. email from Larry
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 blanchet 2010-08-27 merged
2010-08-26 blanchet 2010-08-26 improve SPASS hack, when a clause comes from several facts
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-26 blanchet 2010-08-26 renaming
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-23 blanchet 2010-08-23 cache previous iteration's weights, and keep track of what's dirty and what's clean; this speeds up the relevance filter significantly
2010-08-23 blanchet 2010-08-23 prevent double inclusion of the fact "True_or_False" in TPTP problems
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-20 blanchet 2010-08-20 remove trivial facts
2010-08-20 blanchet 2010-08-20 use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; avoids relying on inconsistently implemented feature of TPTP format
2010-08-20 blanchet 2010-08-20 transform elim theorems before filtering "bool" and "prop" variables out; another consequence of the transition to FOF
2010-08-20 blanchet 2010-08-20 beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly); another consequence of the transition to FOF
2010-08-19 blanchet 2010-08-19 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
2010-08-19 blanchet 2010-08-19 fix atomize
2010-08-19 blanchet 2010-08-19 improve atomization
2010-08-18 blanchet 2010-08-18 added "max_relevant_per_iter" option to Sledgehammer
2010-08-18 blanchet 2010-08-18 handle bound name conflicts gracefully in FOF translation
2010-08-17 blanchet 2010-08-17 repair translation of "c_fequal"
2010-08-17 blanchet 2010-08-17 invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms; this resulted in a subtle soundness bug in Sledgehammer -- introduced by the transition to FOF
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)