2011-08-23 blanchet 2011-08-23 fixed TFF slicing
2011-08-23 blanchet 2011-08-23 kindly ask Vampire to output axiom names
2011-08-23 blanchet 2011-08-23 added formats to the slice and use TFF for remote Vampire
2011-08-22 blanchet 2011-08-22 gracefully handle empty SPASS problems
2011-08-17 blanchet 2011-08-17 distinguish THF syntax with and without choice (Satallax vs. LEO-II)
2011-08-09 blanchet 2011-08-09 support local HOATPs
2011-08-09 blanchet 2011-08-09 LEO-II also supports FOF
2011-08-09 blanchet 2011-08-09 renamed E wrappers for consistency with CASC conventions
2011-07-26 blanchet 2011-07-26 renamed "preds" encodings to "guards"
2011-07-26 blanchet 2011-07-26 give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-07-06 blanchet 2011-07-06 better setup for experimental "z3_atp"
2011-07-01 blanchet 2011-07-01 renamed "type_sys" to "type_enc", which is more accurate
2011-07-01 blanchet 2011-07-01 cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
2011-07-01 blanchet 2011-07-01 tuning
2011-06-27 blanchet 2011-06-27 tweaked comment
2011-06-27 blanchet 2011-06-27 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-27 blanchet 2011-06-27 remove experimental trimming feature -- it slowed down things on Linux for some reason
2011-06-27 blanchet 2011-06-27 filter out some tautologies using an ATP, especially for those theories that are known for producing such things
2011-06-23 blanchet 2011-06-23 fiddle with remote ATP settings, based on Judgment Day
2011-06-21 blanchet 2011-06-21 provide appropriate type system and number of fact defaults for remote ATPs
2011-06-21 blanchet 2011-06-21 tweaked E, SPASS, Vampire setup based on latest Judgment Day results
2011-06-20 blanchet 2011-06-20 slightly better setup for E
2011-06-20 blanchet 2011-06-20 slightly better setup for SPASS and Vampire as more results have come in
2011-06-20 blanchet 2011-06-20 optimized SPASS and Vampire time slices, like E before
2011-06-20 blanchet 2011-06-20 optimized E's time slicing, based on latest exhaustive Judgment Day results
2011-06-20 blanchet 2011-06-20 deal with ATP time slices in a more flexible/robust fashion
2011-06-19 blanchet 2011-06-19 recognize one more E failure message
2011-06-19 blanchet 2011-06-19 tweaked TPTP formula kind for typing information used in the conjecture
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