src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
Thu, 16 Dec 2010 15:46:54 +0100 blanchet no need to do a super-duper atomization if Metis fails afterwards anyway
Thu, 16 Dec 2010 15:12:17 +0100 blanchet instantiate induction rules automatically
Wed, 15 Dec 2010 11:26:29 +0100 blanchet tuning
Wed, 15 Dec 2010 11:26:29 +0100 blanchet make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
Wed, 15 Dec 2010 11:26:29 +0100 blanchet consider "finite" overloaded in "precise_overloaded_args" mode
Wed, 15 Dec 2010 11:26:29 +0100 blanchet fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"
Wed, 15 Dec 2010 11:26:28 +0100 blanchet improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added Sledgehammer support for higher-order propositional reasoning
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
Wed, 15 Dec 2010 11:26:28 +0100 blanchet added "type_sys" option to Sledgehammer
Wed, 08 Dec 2010 22:17:53 +0100 blanchet implicitly call the minimizer for SMT solvers that don't return an unsat core
Wed, 08 Dec 2010 22:17:52 +0100 blanchet clarified terminology
Tue, 26 Oct 2010 21:01:28 +0200 blanchet standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
Tue, 26 Oct 2010 10:57:04 +0200 blanchet no need to encode theorem number twice in skolem names
Fri, 22 Oct 2010 18:31:45 +0200 blanchet tuning
Fri, 22 Oct 2010 14:10:32 +0200 blanchet fixed signature of "is_smt_solver_installed";
Fri, 22 Oct 2010 13:57:54 +0200 blanchet renamed modules
Fri, 22 Oct 2010 13:54:51 +0200 blanchet renamed files
less more (0) tip