src/HOL/Tools/ATP/atp_systems.ML
2010-11-23 blanchet 2010-11-23 more precise error handling for Z3; refactored some of the error handling code shared by ATP and SMT
2010-11-18 blanchet 2010-11-18 remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
2010-11-08 blanchet 2010-11-08 recognize Vampire error
2010-11-03 blanchet 2010-11-03 give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-10-21 blanchet 2010-10-21 first step in adding support for an SMT backend to Sledgehammer
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-09-16 blanchet 2010-09-16 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
2010-09-14 blanchet 2010-09-14 prefer version 0.6 of Vampire, now that we can parse its output
2010-09-11 blanchet 2010-09-11 tuning
2010-09-11 blanchet 2010-09-11 change order of default ATPs; put SPASS first so that it's picked up by Auto Sledgehammer
2010-09-09 blanchet 2010-09-09 more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
2010-09-09 blanchet 2010-09-09 better error reporting when the Sledgehammer minimizer is interrupted
2010-09-08 blanchet 2010-09-08 improve SInE-E failure message
2010-09-02 blanchet 2010-09-02 SNARK doesn't like facts
2010-09-02 blanchet 2010-09-02 show real CPU time
2010-09-01 blanchet 2010-09-01 add dependency of "spass" script
2010-09-01 blanchet 2010-09-01 lower number of facts given to SInE
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-08-26 blanchet 2010-08-26 fix Vampire version numbers
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 make SML/NJ happy
2010-08-24 blanchet 2010-08-24 better workaround for E's off-by-one-second issue
2010-08-24 blanchet 2010-08-24 use a soft time limit for E with a hard limit, "eproof"/"eproof.pl" doesn't show the proof is there's less than 1 second left, yielding "the ATP output is malformed"
2010-08-24 blanchet 2010-08-24 make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
2010-08-23 blanchet 2010-08-23 adjust fudge factors in the light of experiments
2010-08-23 blanchet 2010-08-23 revert unintended change
2010-08-23 blanchet 2010-08-23 prevent double inclusion of the fact "True_or_False" in TPTP problems
2010-08-23 blanchet 2010-08-23 play with fudge factor + parse one more Vampire error
2010-08-23 blanchet 2010-08-23 fiddle a bit with the SPASS fudge number
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 fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
2010-08-19 blanchet 2010-08-19 added remote SInE and remote SNARK
2010-08-18 blanchet 2010-08-18 don't get confused by wrong slice
2010-08-18 blanchet 2010-08-18 added "max_relevant_per_iter" option to Sledgehammer
2010-08-18 blanchet 2010-08-18 thank Andrei instead of Tanya
2010-08-18 blanchet 2010-08-18 rename enum values
2010-08-17 blanchet 2010-08-17 tweaking
2010-08-17 blanchet 2010-08-17 merged
2010-08-17 blanchet 2010-08-17 improve detection of old Vampire versions
2010-08-17 wenzelm 2010-08-17 made 9043eefe8d71 actually compile;
2010-08-16 blanchet 2010-08-16 detect old Vampire and give a nicer error message
2010-08-16 blanchet 2010-08-16 Geoff's formatter now needs closed formulas
2010-08-09 blanchet 2010-08-09 fiddle some more with "max_new_relevant_facts_per_iter"
2010-07-29 blanchet 2010-07-29 avoid "ATP Error: Error: blah" style messages
2010-07-29 blanchet 2010-07-29 better error and minimizer output
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 fiddle with the fudge factors, to get similar results as before
2010-07-29 blanchet 2010-07-29 improved ATP error handling some more
2010-07-29 blanchet 2010-07-29 shorter URL
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 renamed environment variable
2010-07-28 blanchet 2010-07-28 consequence of directory renaming
2010-07-28 blanchet 2010-07-28 rename directory