src/HOL/Tools/ATP/atp_systems.ML
2012-03-20 blanchet 2012-03-20 implement term order attribute (for experiments)
2012-03-20 blanchet 2012-03-20 tuning -- don't refer to old, internal version number (needlessly confusing now)
2012-03-20 blanchet 2012-03-20 more weight attribute tuning
2012-03-20 blanchet 2012-03-20 use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0
2012-03-20 blanchet 2012-03-20 internal renamings
2012-03-20 blanchet 2012-03-20 renamed E weight attribute
2012-02-24 blanchet 2012-02-24 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-14 blanchet 2012-02-14 don't report spurious LEO-II errors
2012-02-14 blanchet 2012-02-14 better error message
2012-02-11 blanchet 2012-02-11 new SPASS options
2012-02-10 blanchet 2012-02-10 update SPASS slices
2012-02-09 blanchet 2012-02-09 new SPASS slices
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-05 blanchet 2012-02-05 remove option that's on by default
2012-02-05 blanchet 2012-02-05 no need for a script/mega-hack with the new SPASS
2012-02-05 blanchet 2012-02-05 cleaned up new SPASS parsing
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-02-03 blanchet 2012-02-03 optimization: slice caching in case two consecutive slices are nearly identical
2012-02-02 blanchet 2012-02-02 change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02 blanchet 2012-02-02 better SPASS setup
2012-02-02 blanchet 2012-02-02 include new SPASS by default if available
2012-01-31 blanchet 2012-01-31 third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31 blanchet 2012-01-31 improve SPASS setup
2012-01-31 blanchet 2012-01-31 fixed syntax bug in DFG output
2012-01-31 blanchet 2012-01-31 new SPASS setup
2012-01-30 blanchet 2012-01-30 new SPASS setup
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-23 blanchet 2012-01-23 renamed two files to make room for a new file
2011-12-14 blanchet 2011-12-14 SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
2011-11-16 blanchet 2011-11-16 give each time slice its own lambda translation
2011-11-06 blanchet 2011-11-06 renamed experimental systems
2011-11-04 blanchet 2011-11-04 document new experimental provers
2011-11-04 blanchet 2011-11-04 added remote iProver(-Eq) for experimentation
2011-10-29 blanchet 2011-10-29 always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
2011-10-29 blanchet 2011-10-29 added DFG unsorted support (like in the old days)
2011-10-29 blanchet 2011-10-29 added sorted DFG output for coming version of SPASS
2011-10-29 blanchet 2011-10-29 specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
2011-10-21 blanchet 2011-10-21 disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction
2011-10-19 blanchet 2011-10-19 one more LEO-II failure
2011-10-19 blanchet 2011-10-19 more uniform SZS status handling
2011-10-17 blanchet 2011-10-17 parse Satallax unsat cores
2011-09-07 blanchet 2011-09-07 tweaking polymorphic TFF and THF output
2011-09-07 blanchet 2011-09-07 rationalize uniform encodings
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"