src/HOL/Tools/ATP/atp_systems.ML
2011-05-01 blanchet 2011-05-01 recognize more SystemOnTPTP errors
2011-05-01 blanchet 2011-05-01 better known failure recognition for ToFoF-E
2011-05-01 blanchet 2011-05-01 improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
2011-05-01 blanchet 2011-05-01 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
2011-05-01 blanchet 2011-05-01 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-04-14 blanchet 2011-04-14 handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
2011-02-18 blanchet 2011-02-18 adjust fudge factors
2011-02-18 blanchet 2011-02-18 extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
2011-02-15 blanchet 2011-02-15 make experimental "Z3 ATP" work on Linux as well
2011-02-15 blanchet 2011-02-15 adjusted fudge factors (based on Judgment Day runs)
2011-02-10 blanchet 2011-02-10 make minimizer verbose
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