src/HOL/Tools/Sledgehammer/sledgehammer.ML
2010-09-08 blanchet 2010-09-08 merge
2010-09-06 blanchet 2010-09-06 use Future.fork rather than Thread.fork, so that the thread is part of the global thread management
2010-09-06 wenzelm 2010-09-06 some results of concurrency code inspection;
2010-09-02 blanchet 2010-09-02 show the number of facts for each prover in "verbose" mode
2010-09-02 blanchet 2010-09-02 make sure "Unknown ATP" errors reach the users -- i.e. don't generate them from a thread
2010-09-02 blanchet 2010-09-02 If Geoff puts some important message in his TPTP problems (e.g., money requests), we should show them to the user
2010-09-02 blanchet 2010-09-02 show real CPU time
2010-09-01 blanchet 2010-09-01 factor out code shared by all ATPs so that it's run only once
2010-09-01 blanchet 2010-09-01 handle all whitespace, not just ASCII 32
2010-09-01 blanchet 2010-09-01 speed up SPASS hack + output time information in "blocking" mode
2010-09-01 blanchet 2010-09-01 minor refactoring
2010-09-01 blanchet 2010-09-01 translate the axioms to FOF once and for all ATPs
2010-09-01 blanchet 2010-09-01 run relevance filter in a thread, to avoid blocking
2010-09-01 blanchet 2010-09-01 only kill ATP threads in nonblocking mode
2010-09-01 blanchet 2010-09-01 share the relevance filter among the provers
2010-09-01 blanchet 2010-09-01 got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers
2010-09-01 blanchet 2010-09-01 rename sledgehammer config attributes
2010-08-31 blanchet 2010-08-31 finished renaming
2010-08-31 blanchet 2010-08-31 added "expect" feature of Nitpick to Sledgehammer, for regression testing
2010-08-31 blanchet 2010-08-31 added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing
2010-08-30 blanchet 2010-08-30 remove useless var
2010-08-30 blanchet 2010-08-30 remove needless parameter
2010-08-26 blanchet 2010-08-26 improve SPASS hack, when a clause comes from several facts
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-26 blanchet 2010-08-26 renaming
2010-08-25 blanchet 2010-08-25 reorganize options regarding to the relevance threshold and decay
2010-08-25 blanchet 2010-08-25 make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)
2010-08-25 blanchet 2010-08-25 get rid of "defs_relevant" feature; nobody uses it and it works poorly
2010-08-25 blanchet 2010-08-25 renamed "relevance_convergence" to "relevance_decay"
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-24 blanchet 2010-08-24 clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name
2010-08-23 blanchet 2010-08-23 weed out junk in relevance filter
2010-08-22 blanchet 2010-08-22 be more generous towards SPASS's -SOS mode
2010-08-22 blanchet 2010-08-22 prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.
2010-08-19 blanchet 2010-08-19 tuning
2010-08-19 blanchet 2010-08-19 no spurious trailing "\n" at the end of Sledgehammer's output
2010-08-18 blanchet 2010-08-18 get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
2010-08-18 blanchet 2010-08-18 added "max_relevant_per_iter" option to Sledgehammer
2010-08-18 blanchet 2010-08-18 improve SPASS clause numbering hack
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