src/HOL/Tools/ATP/atp_systems.ML
2011-02-09 blanchet 2011-02-09 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
2011-02-09 blanchet 2011-02-09 renamed field
2011-02-09 blanchet 2011-02-09 added "Z3 as an ATP" support to Sledgehammer locally
2011-02-09 blanchet 2011-02-09 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
2011-02-08 blanchet 2011-02-08 available_provers ~> supported_provers (for clarity)
2011-02-08 blanchet 2011-02-08 added support for bleeding-edge E weighting function "SymOffsetsWeight"
2010-12-21 blanchet 2010-12-21 added "smt_triggers" option to experiment with triggers in Sledgehammer; renamings (for consistency)
2010-12-21 blanchet 2010-12-21 enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
2010-12-20 blanchet 2010-12-20 disable feature that was enabled by mistake
2010-12-20 blanchet 2010-12-20 use the options provided by Stephan Schulz -- much better
2010-12-20 blanchet 2010-12-20 optionally supply constant weights to E -- turned off by default until properly parameterized
2010-12-18 blanchet 2010-12-18 tuning
2010-12-17 blanchet 2010-12-17 fewer facts to SInE-E
2010-12-16 blanchet 2010-12-16 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
2010-12-15 blanchet 2010-12-15 added timeout max for remote server invocation
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