src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2011-05-01 blanchet 2011-05-01 make sure typing fact names are unique (needed e.g. by SNARK)
2011-05-01 blanchet 2011-05-01 minor cleanup
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 declare TFF types so that SNARK can be used with types
2011-05-01 blanchet 2011-05-01 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
2011-05-01 blanchet 2011-05-01 move type declarations to the front, for TFF-compliance
2011-05-01 blanchet 2011-05-01 use postfix syntax for mangled types, for consistency with unmangled
2011-05-01 blanchet 2011-05-01 generate typing for "hBOOL" in "Many_Typed" mode + tuning
2011-05-01 blanchet 2011-05-01 generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
2011-05-01 blanchet 2011-05-01 fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
2011-05-01 blanchet 2011-05-01 generate TFF type declarations in typed mode
2011-05-01 blanchet 2011-05-01 added more rudimentary type support to Sledgehammer's ATP encoding
2011-05-01 blanchet 2011-05-01 fixed type of ATP quantifier types (sic)
2011-05-01 blanchet 2011-05-01 added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS
2011-05-01 blanchet 2011-05-01 added support for TFF type declarations
2011-05-01 blanchet 2011-05-01 reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter
2011-05-01 blanchet 2011-05-01 added room for types in ATP quantifiers
2011-05-01 blanchet 2011-05-01 distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
2011-05-01 blanchet 2011-05-01 remove experimental feature ("risky overload")
2011-05-01 blanchet 2011-05-01 added (without implementation yet) new type encodings for Sledgehammer/ATP
2011-05-01 blanchet 2011-05-01 close ATP formulas universally earlier, so that we can add type predicates
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