src/HOL/Tools/Sledgehammer/sledgehammer.ML
2010-08-16 blanchet 2010-08-16 more debug output
2010-08-09 blanchet 2010-08-09 prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch
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 reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF
2010-08-09 blanchet 2010-08-09 fix embarrassing bug in elim rule handling, introduced during the port to FOF
2010-08-05 blanchet 2010-08-05 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-07-30 blanchet 2010-07-30 don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...
2010-07-29 blanchet 2010-07-29 fix bug in the newly introduced "bound concealing" code
2010-07-29 blanchet 2010-07-29 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses
2010-07-29 blanchet 2010-07-29 handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
2010-07-29 blanchet 2010-07-29 speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
2010-07-29 blanchet 2010-07-29 work around atomization failures
2010-07-29 blanchet 2010-07-29 perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
2010-07-29 blanchet 2010-07-29 fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
2010-07-29 blanchet 2010-07-29 generate correct names for "$true" and "$false"; this was lost somewhere in the non-clausification
2010-07-29 blanchet 2010-07-29 don't assume canonical rule format
2010-07-29 blanchet 2010-07-29 avoid "clause" and "cnf" terminology where it no longer makes sense
2010-07-29 blanchet 2010-07-29 "axiom_clauses" -> "axioms" (these are no longer clauses)
2010-07-29 blanchet 2010-07-29 remove the "extra_clauses" business introduced in 19a5f1c8a844; it isn't working reliably because of: * relevance_override * it is ignored anyway by TPTP generator A better solution would/will be to ensure monotonicity: extra axioms not used in an ATP proof shouldn't make the rest of the problem provable
2010-07-28 blanchet 2010-07-28 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
2010-07-28 blanchet 2010-07-28 minor refactoring
2010-07-28 blanchet 2010-07-28 fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
2010-07-28 blanchet 2010-07-28 revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well; we can no longer just count the formulas, because for some reason E's numbering either no longer starts at 1 or it doesn't increment by 1 at each step
2010-07-28 blanchet 2010-07-28 renaming
2010-07-28 blanchet 2010-07-28 improve detection of installed SPASS
2010-07-27 blanchet 2010-07-27 minor refactoring
2010-07-27 blanchet 2010-07-27 more refactoring
2010-07-27 blanchet 2010-07-27 rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come
2010-07-27 blanchet 2010-07-27 rename