src/HOL/Tools/ATP/atp_systems.ML
2014-07-25 blanchet 2014-07-25 tuning
2014-07-25 blanchet 2014-07-25 avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
2014-07-24 blanchet 2014-07-24 stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-12 blanchet 2014-07-12 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
2014-06-24 blanchet 2014-06-24 added 'dummy_thf_ml' prover for experiments with HOLyHammer
2014-06-17 blanchet 2014-06-17 changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
2014-06-16 blanchet 2014-06-16 use right delimiters for Waldmeister proofs
2014-06-16 blanchet 2014-06-16 added 'waldmeister_new' as ATP
2014-06-16 blanchet 2014-06-16 moved code around
2014-06-16 blanchet 2014-06-16 give Z3 TPTP proofs a chance
2014-06-16 fleury 2014-06-16 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-06-02 fleury 2014-06-02 basic setup for zipperposition prover
2014-05-19 blanchet 2014-05-19 use E 1.8's auto scheduler option
2014-05-04 blanchet 2014-05-04 added missing space between command-line options
2014-04-04 blanchet 2014-04-04 use Z3 TPTP cores rather than proofs since the latter are somewhat broken
2014-04-04 blanchet 2014-04-04 improved parsing of "z3_tptp" proofs
2014-04-03 blanchet 2014-04-03 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
2014-04-03 blanchet 2014-04-03 use Alt-Ergo 0.95.2, the latest and greatest version
2014-04-03 blanchet 2014-04-03 updated Z3 TPTP to 4.3.1+
2013-12-18 blanchet 2013-12-18 made SML/NJ happier
2013-12-17 blanchet 2013-12-17 primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
2013-10-24 blanchet 2013-10-24 use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
2013-09-11 blanchet 2013-09-11 adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
2013-08-28 blanchet 2013-08-28 got rid of old error -- users who install SPASS manually are responsible for any version mismatches
2013-08-13 blanchet 2013-08-13 Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
2013-07-29 blanchet 2013-07-29 added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
2013-05-26 blanchet 2013-05-26 disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
2013-05-21 blanchet 2013-05-21 disabled choice in Satallax
2013-05-21 blanchet 2013-05-21 prefer compiled version of LEO-II and Satallax if available
2013-05-21 blanchet 2013-05-21 updated remote provers
2013-05-20 blanchet 2013-05-20 started adding agsyHOL as an experimental prover
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-08 blanchet 2013-05-08 use right default for "uncurried_aliases" with polymorphic SPASS
2013-05-03 blanchet 2013-05-03 tuning
2013-05-03 blanchet 2013-05-03 pass certain readability-enhancing Vampire options only when an Isar proof is needed
2013-04-08 blanchet 2013-04-08 robustness w.r.t. unknown arguments
2013-03-20 blanchet 2013-03-20 use the right role for SPASS hypotheses
2013-03-05 blanchet 2013-03-05 polymorphic SPASS is also SPASS
2013-02-21 blanchet 2013-02-21 swap slices so that the last slice is more complete (for minimization)
2013-02-20 blanchet 2013-02-20 upgraded to Alt-Ergo 0.95
2013-02-20 blanchet 2013-02-20 turn off more evil Vampire options to facilitate Isar proof generation
2013-02-03 blanchet 2013-02-03 tuned slicing (E-MaLeS and E-Par)
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