src/HOL/Tools/Sledgehammer/clausifier.ML
2010-09-20 blanchet 2010-09-20 remove needless exception
2010-09-14 blanchet 2010-09-14 tuning
2010-09-14 blanchet 2010-09-14 rename internal Sledgehammer constant
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-09 blanchet 2010-09-09 use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way
2010-09-09 blanchet 2010-09-09 add cutoff beyond which facts are handled using definitional CNF
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-09-03 blanchet 2010-09-03 disable "definitional CNF"; it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method
2010-09-02 blanchet 2010-09-02 Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
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-22 blanchet 2010-08-22 treat "using X by metis" (more or less) the same as "by (metis X)"
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-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-09 blanchet 2010-08-09 replace recursion with "fold"
2010-08-09 blanchet 2010-08-09 remove now needless "Thm.transfer"
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 get rid of more dead wood
2010-07-26 blanchet 2010-07-26 prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
2010-07-26 blanchet 2010-07-26 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
2010-07-26 blanchet 2010-07-26 added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-06-29 blanchet 2010-06-29 more elegant cheating
2010-06-29 blanchet 2010-06-29 Sledgehammer can save some msecs by cheating
2010-06-29 blanchet 2010-06-29 move blacklisting completely out of the clausifier; the only reason it was in the clausifier as well was the Skolem cache
2010-06-28 blanchet 2010-06-28 remove obsolete component of CNF clause tuple (and reorder it)
2010-06-28 blanchet 2010-06-28 get rid of Skolem cache by performing CNF-conversion after fact selection
2010-06-28 blanchet 2010-06-28 always perform "inline" skolemization, polymorphism or not, Skolem cache or not
2010-06-28 blanchet 2010-06-28 always perform relevance filtering on original formulas
2010-06-25 blanchet 2010-06-25 factor out thread creation
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)