src/HOL/Tools/ATP/atp_systems.ML
2011-06-10 blanchet 2011-06-10 pass --trim option to "eproof" script to speed up proof reconstruction
2011-06-08 blanchet 2011-06-08 better default type system for Waldmeister, with fewer predicates (for types or type classes)
2011-06-06 blanchet 2011-06-06 slighly more reasonable Vampire slices (until new monomorphizer is used)
2011-05-30 blanchet 2011-05-30 avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
2011-05-30 blanchet 2011-05-30 no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
2011-05-30 blanchet 2011-05-30 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-27 blanchet 2011-05-27 recognize more ATP failures
2011-05-24 blanchet 2011-05-24 ensure that the argument of logical negation is enclosed in parentheses in THF mode
2011-05-24 blanchet 2011-05-24 further reduce the number of facts passed to less used remote ATPs
2011-05-24 blanchet 2011-05-24 pass fewer relevant facts to less used remote systems
2011-05-24 blanchet 2011-05-24 slightly gracefuller handling of LEO-II and Satallax output
2011-05-24 blanchet 2011-05-24 identify HOL functions with THF functions
2011-05-24 blanchet 2011-05-24 started adding support for THF output (but no lambdas)
2011-05-24 blanchet 2011-05-24 clearer SystemOnTPTP errors
2011-05-24 blanchet 2011-05-24 give fewer equations to Waldmeister
2011-05-24 blanchet 2011-05-24 detect inappropriate problems and crashes better in Waldmeister
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-22 blanchet 2011-05-22 fish out axioms in Waldmeister output
2011-05-22 blanchet 2011-05-22 recognize one more SystemOnTPTP error
2011-05-22 blanchet 2011-05-22 added support for remote Waldmeister
2011-05-22 blanchet 2011-05-22 added Waldmeister
2011-05-22 blanchet 2011-05-22 reorganized ATP formats a little bit
2011-05-20 blanchet 2011-05-20 make sure the Vampire incomplete proof detection code kicks in
2011-05-19 blanchet 2011-05-19 renamed "simple_types" to "simple"
2011-05-19 blanchet 2011-05-19 tweaked ATP type systems further based on Judgment Day
2011-05-19 blanchet 2011-05-19 better error reporting: detect missing E proofs and remove Vampire native format error
2011-05-13 blanchet 2011-05-13 tweak E slices
2011-05-12 blanchet 2011-05-12 drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
2011-05-12 blanchet 2011-05-12 added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
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)