src/HOL/Tools/ATP/atp_systems.ML
2013-02-02 blanchet 2013-02-02 tune slices further
2013-02-02 blanchet 2013-02-02 tweak ATP slices further
2013-01-31 blanchet 2013-01-31 tuned slices
2013-01-31 blanchet 2013-01-31 store fact filter along with ATP slice
2013-01-17 blanchet 2013-01-17 make SPASS more configurable, for experiments
2013-01-17 blanchet 2013-01-17 added E-Par support
2012-12-03 blanchet 2012-12-03 tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
2012-10-31 blanchet 2012-10-31 less verbose -- the warning will reach the users anyway by other means
2012-10-31 blanchet 2012-10-31 tuned messages
2012-10-31 blanchet 2012-10-31 added a timeout around script that relies on the network
2012-10-31 blanchet 2012-10-31 tuning
2012-08-14 blanchet 2012-08-14 tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
2012-08-14 blanchet 2012-08-14 tweak Vampire setup in the light of new evaluation
2012-08-07 blanchet 2012-08-07 proper quoting
2012-08-07 blanchet 2012-08-07 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-08-07 blanchet 2012-08-07 specify full path to clausifier
2012-08-06 blanchet 2012-08-06 added iProver(-Eq) local
2012-08-02 blanchet 2012-08-02 support older versions of Vampire
2012-08-02 blanchet 2012-08-02 added E-MaLeS to list of provers for testing
2012-07-27 blanchet 2012-07-27 tweaks in preparation for type encoding evaluation
2012-07-27 blanchet 2012-07-27 extract Z3 unsat cores (for "z3_tptp")
2012-07-20 blanchet 2012-07-20 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
2012-07-10 blanchet 2012-07-10 don't ask E to generate a detailed proofs if not needed
2012-06-26 blanchet 2012-06-26 started adding polymophic SPASS output
2012-06-26 blanchet 2012-06-26 tuning
2012-06-26 blanchet 2012-06-26 removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
2012-06-06 blanchet 2012-06-06 pass more facts to LEO-II, in the light of latest evaluation
2012-06-06 blanchet 2012-06-06 robust LEO-II setup that doesn't rely on ".leoatprc"
2012-06-06 blanchet 2012-06-06 tweaked remote Vampire version
2012-05-28 blanchet 2012-05-28 tweaked remote Vampire setup
2012-05-28 blanchet 2012-05-28 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
2012-05-28 blanchet 2012-05-28 don't generate definitions for LEO-II -- this cuases more harm than good
2012-05-24 blanchet 2012-05-24 update Satallax setup based on evaluation
2012-05-24 blanchet 2012-05-24 gracefully handle definition-looking premises
2012-05-23 blanchet 2012-05-23 tuned names
2012-05-23 blanchet 2012-05-23 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
2012-05-23 blanchet 2012-05-23 better handling of incomplete TSTP proofs
2012-05-23 blanchet 2012-05-23 lower the monomorphization thresholds for less scalable provers
2012-05-22 blanchet 2012-05-22 added one slice with configurable simplification turned off
2012-05-21 blanchet 2012-05-21 invite users to upgrade their SPASS (so we can get rid of old code)
2012-05-21 blanchet 2012-05-21 start phasing out old SPASS
2012-05-21 blanchet 2012-05-21 minor tweak in Vampire setup
2012-05-16 blanchet 2012-05-16 minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
2012-05-14 blanchet 2012-05-14 tuning
2012-05-13 blanchet 2012-05-13 LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
2012-05-13 blanchet 2012-05-13 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
2012-05-10 blanchet 2012-05-10 pass fewer facts to LEO-II and Satallax
2012-05-10 blanchet 2012-05-10 tweak LEO-II setup
2012-05-10 blanchet 2012-05-10 use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
2012-04-27 blanchet 2012-04-27 tweak LEO-II setup
2012-04-26 blanchet 2012-04-26 tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
2012-04-24 blanchet 2012-04-24 removed confusing error
2012-04-22 blanchet 2012-04-22 tried harder to make SML/NJ happy
2012-04-21 blanchet 2012-04-21 tried to make SML/NJ happy
2012-04-19 blanchet 2012-04-19 true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-17 blanchet 2012-04-17 more helpful error message
2012-04-17 blanchet 2012-04-17 avoid option introduced in E 1.2 when invoking older versions of E
2012-04-16 wenzelm 2012-04-16 redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
2012-03-27 blanchet 2012-03-27 tweak slices, based on eval by Daniel Wand
2012-03-21 blanchet 2012-03-21 removed Satallax option, now that this is the default