src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2011-05-01 blanchet 2011-05-01 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
2011-05-01 blanchet 2011-05-01 renamings
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-14 blanchet 2011-04-14 correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
2011-04-05 blanchet 2011-04-05 renamed "const_args" option value to "args"
2011-04-05 blanchet 2011-04-05 temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
2011-04-05 blanchet 2011-04-05 killed unimplemented type encoding "preds"
2011-04-05 blanchet 2011-04-05 remove debugging code
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-03-17 blanchet 2011-03-17 add option to function to keep trivial ATP formulas, needed for some experiments
2011-02-18 blanchet 2011-02-18 adjust fudge factors
2011-02-18 blanchet 2011-02-18 extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
2011-02-10 blanchet 2011-02-10 fix handling of "fequal" in generated ATP problems -- the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
2011-02-08 blanchet 2011-02-08 sort E weights
2011-01-10 wenzelm 2011-01-10 eliminated Int.toString;
2010-12-28 wenzelm 2010-12-28 made SML/NJ happy;
2010-12-22 blanchet 2010-12-22 made SML/NJ happy
2010-12-20 blanchet 2010-12-20 optionally supply constant weights to E -- turned off by default until properly parameterized
2010-12-16 blanchet 2010-12-16 no need to do a super-duper atomization if Metis fails afterwards anyway
2010-12-16 blanchet 2010-12-16 instantiate induction rules automatically
2010-12-15 blanchet 2010-12-15 tuning
2010-12-15 blanchet 2010-12-15 make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
2010-12-15 blanchet 2010-12-15 consider "finite" overloaded in "precise_overloaded_args" mode
2010-12-15 blanchet 2010-12-15 fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"
2010-12-15 blanchet 2010-12-15 improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
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 "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
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-12-15 blanchet 2010-12-15 added "type_sys" option to Sledgehammer
2010-12-08 blanchet 2010-12-08 implicitly call the minimizer for SMT solvers that don't return an unsat core
2010-12-08 blanchet 2010-12-08 clarified terminology
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-26 blanchet 2010-10-26 no need to encode theorem number twice in skolem names
2010-10-22 blanchet 2010-10-22 tuning
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