src/HOL/Tools/ATP/atp_systems.ML
2011-05-12 blanchet 2011-05-12 allow each slice to have its own type system
2011-05-06 blanchet 2011-05-06 further improved type system setup based on Judgment Days
2011-05-06 blanchet 2011-05-06 allow each prover to specify its own formula kind for symbols occurring in the conjecture
2011-05-06 blanchet 2011-05-06 better type system setup, based on Judgment Day
2011-05-05 blanchet 2011-05-05 improve suggested type system list based on evaluation
2011-05-04 blanchet 2011-05-04 renamed "many_typed" to "simple" (as in simple types)
2011-05-04 blanchet 2011-05-04 added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
2011-05-03 blanchet 2011-05-03 whitespace tuning
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet 2011-05-02 better default type systems for SNARK and ToFoF
2011-05-02 blanchet 2011-05-02 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-02 blanchet 2011-05-02 supply type-system defaults for major ATPs
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 pick up GaveUp error on SystemOnTPTP
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-05-01 blanchet 2011-05-01 define type system in ATP module so that ATPs can suggest a type system
2011-05-01 blanchet 2011-05-01 made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
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