src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
2011-05-01 blanchet 2011-05-01 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-05-01 blanchet 2011-05-01 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
2011-05-01 blanchet 2011-05-01 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
2011-05-01 blanchet 2011-05-01 improve helper type instantiation code
2011-05-01 blanchet 2011-05-01 killed needless datatype "combtyp" in Metis
2011-05-01 blanchet 2011-05-01 added friendly hint when Isar proof is missing
2011-05-01 blanchet 2011-05-01 reconstruct TFF type predicates correctly for ToFoF
2011-05-01 blanchet 2011-05-01 handle special constants correctly in Isar proof reconstruction code, especially type predicates
2011-05-01 blanchet 2011-05-01 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
2011-05-01 blanchet 2011-05-01 move type declarations to the front, for TFF-compliance
2011-05-01 blanchet 2011-05-01 generate typing for "hBOOL" in "Many_Typed" mode + tuning
2011-05-01 blanchet 2011-05-01 added more rudimentary type support to Sledgehammer's ATP encoding
2011-05-01 blanchet 2011-05-01 added room for types in ATP quantifiers
2011-04-22 blanchet 2011-04-22 automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-04 blanchet 2011-04-04 if "monomorphize" is enabled, mangle the type information in the names by default
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2010-12-16 blanchet 2010-12-16 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
2010-12-15 blanchet 2010-12-15 generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
2010-12-15 blanchet 2010-12-15 fix Vampire parsing problem
2010-12-15 blanchet 2010-12-15 added Sledgehammer support for higher-order propositional reasoning
2010-12-15 blanchet 2010-12-15 implemented partially-typed "tags" type encoding
2010-12-15 blanchet 2010-12-15 implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
2010-11-26 blanchet 2010-11-26 put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-10-26 blanchet 2010-10-26 standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
2010-10-22 blanchet 2010-10-22 tuning
2010-10-22 blanchet 2010-10-22 compile
2010-10-22 blanchet 2010-10-22 fixed signature of "is_smt_solver_installed"; renaming
2010-10-22 blanchet 2010-10-22 renamed modules
2010-10-22 blanchet 2010-10-22 renamed files