src/HOL/Tools/ATP/atp_systems.ML
17 months ago blanchet 2017-11-07 integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
20 months ago blanchet 2017-08-29 improved Vampire proof parser
20 months ago blanchet 2017-08-07 use TFF0 with E 2.0 and above
20 months ago blanchet 2017-08-07 updated remote Vampire version
2016-09-02 blanchet 2016-09-02 adapted remote E
2016-08-14 blanchet 2016-08-14 killed final stops in Sledgehammer and friends
2016-05-23 blanchet 2016-05-23 generate Vampire 4.0 compatible output
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-03-03 blanchet 2015-03-03 SPASS-Pirate is now called Pirate
2014-12-03 blanchet 2014-12-03 prefer E 1.8, now that it's been tried and tested
2014-09-30 blanchet 2014-09-30 use native encoding with Vampire -- modern versions handle types better than the old ones
2014-09-29 blanchet 2014-09-29 added option to get cleaner SPASS proofs
2014-08-28 blanchet 2014-08-28 pass options to remote Vampire
2014-08-01 blanchet 2014-08-01 more precise handling of LEO-II skolemization
2014-07-30 fleury 2014-07-30 imported patch satallax_proof_support_Sledgehammer
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