src/HOL/Tools/ATP/atp_proof.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 tuned messages
20 months ago blanchet 2017-08-29 improved Vampire proof parser
20 months ago blanchet 2017-08-15 extended TSTP type parser + tuned messages
2016-08-14 blanchet 2016-08-14 killed final stops in Sledgehammer and friends
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-05 blanchet 2015-10-05 added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
2015-08-27 blanchet 2015-08-27 robust handling of Vampire 4 proofs
2015-03-03 blanchet 2015-03-03 SPASS-Pirate is now called Pirate
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-12 blanchet 2014-10-12 special treatment of extensionality in minimizer
2014-10-06 blanchet 2014-10-06 get rid of 'individual' type in DFG proofs
2014-09-29 blanchet 2014-09-29 parse back type of SPASS proof variables
2014-09-12 fleury 2014-09-12 correction in the thf0 parser ("(=)" found in a Satallax proof).
2014-08-28 blanchet 2014-08-28 reworked unskolemization for SPASS
2014-08-28 blanchet 2014-08-28 tuned message
2014-08-04 blanchet 2014-08-04 tuned comments
2014-08-04 blanchet 2014-08-04 deal with E definitions
2014-07-30 fleury 2014-07-30 Improving robustness and indentation corrections.
2014-07-30 fleury 2014-07-30 Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30 fleury 2014-07-30 imported patch hilbert_choice_support
2014-07-30 fleury 2014-07-30 imported patch satallax_proof_support_Sledgehammer
2014-07-28 blanchet 2014-07-28 correctly translate THF functions from terms to types
2014-07-24 blanchet 2014-07-24 filter out 'theory(...)' from dependencies early on
2014-06-24 blanchet 2014-06-24 added 'dummy_thf_ml' prover for experiments with HOLyHammer
2014-06-16 blanchet 2014-06-16 fixed parsing of one-argument 'file()' in TSTP files
2014-06-16 blanchet 2014-06-16 give Z3 TPTP proofs a chance
2014-06-16 fleury 2014-06-16 Moving the remote prefix deleting on Sledgehammer's side
2014-06-16 fleury 2014-06-16 Correcting the type parser
2014-06-16 fleury 2014-06-16 imported patch leo2_skolem_simplication
2014-06-16 fleury 2014-06-16 add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-06-11 blanchet 2014-06-11 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-10 blanchet 2014-06-10 tuning
2014-06-02 fleury 2014-06-02 basic setup for zipperposition prover
2014-05-20 blanchet 2014-05-20 tuning
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-01-30 blanchet 2014-01-30 unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer
2013-12-20 blanchet 2013-12-20 recognize datatype reasoning in SPASS-Pirate
2013-12-19 blanchet 2013-12-19 extended ATP types with sorts
2013-12-18 blanchet 2013-12-18 parse SPASS-Pirate types
2013-12-18 blanchet 2013-12-18 fixed variable confusion introduced by 'tuning' change 565f9af86d67
2013-12-18 blanchet 2013-12-18 tuning
2013-12-17 blanchet 2013-12-17 primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
2013-12-16 blanchet 2013-12-16 handle Skolems gracefully for SPASS as well
2013-12-16 blanchet 2013-12-16 correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
2013-09-12 blanchet 2013-09-12 generalized data structure, for extension with SMT solver proofs
2013-09-12 blanchet 2013-09-12 prefixed types and some functions with "atp_" for disambiguation
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-28 blanchet 2013-08-28 tuned messages
2013-08-13 blanchet 2013-08-13 more robust parsing of Vampire proofs with "introduced" names
2013-07-29 blanchet 2013-07-29 parse nonnumeric identifiers in E proofs correctly
2013-07-29 blanchet 2013-07-29 simplified Vampire hack -- no need to run it for other ATPs
2013-05-20 blanchet 2013-05-20 parse agsyHOL proofs (as unsat cores)
2013-05-20 blanchet 2013-05-20 started adding agsyHOL as an experimental prover
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-15 blanchet 2013-05-15 renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-06 smolkas 2013-05-06 undo 46d911ab9170 since it causes problems
2013-05-06 smolkas 2013-05-06 allow '-'s in tptp ids to avoid problems with remote_vampire
2013-03-07 blanchet 2013-03-07 better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)