src/HOL/Tools/ATP/atp_systems.ML
2011-09-06 blanchet 2011-09-06 added dummy polymorphic THF system
2011-08-30 blanchet 2011-08-30 cleaner "pff" dummy TFF0 prover
2011-08-30 blanchet 2011-08-30 extended simple types with polymorphism -- the implementation still needs some work though
2011-08-30 blanchet 2011-08-30 added dummy PFF prover, for debugging purposes
2011-08-30 blanchet 2011-08-30 first step towards polymorphic TFF + changed defaults for Vampire
2011-08-30 nik 2011-08-30 improved handling of induction rules in Sledgehammer
2011-08-30 nik 2011-08-30 added generation of induction rules
2011-08-26 blanchet 2011-08-26 disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
2011-08-25 blanchet 2011-08-25 make sure that if slicing is disabled, a non-SOS slice is chosen
2011-08-25 blanchet 2011-08-25 make TFF output less explicit where possible
2011-08-25 blanchet 2011-08-25 use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
2011-08-25 blanchet 2011-08-25 added one more known Z3 failure
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-24 blanchet 2011-08-24 remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
2011-08-23 blanchet 2011-08-23 fixed "hBOOL" of existential variables, and generate more helpers
2011-08-23 blanchet 2011-08-23 always use TFF if possible
2011-08-23 blanchet 2011-08-23 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23 blanchet 2011-08-23 updated known failures for Z3 3.0 TPTP
2011-08-23 blanchet 2011-08-23 avoid TFF format with older Vampire versions
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