src/HOL/Tools/ATP/atp_systems.ML
Tue, 30 Sep 2014 14:18:07 +0200 blanchet use native encoding with Vampire -- modern versions handle types better than the old ones
Mon, 29 Sep 2014 12:29:52 +0200 blanchet added option to get cleaner SPASS proofs
Thu, 28 Aug 2014 16:58:27 +0200 blanchet pass options to remote Vampire
Fri, 01 Aug 2014 19:32:10 +0200 blanchet more precise handling of LEO-II skolemization
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer
Fri, 25 Jul 2014 11:26:19 +0200 blanchet tuning
Fri, 25 Jul 2014 11:26:17 +0200 blanchet avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
Thu, 24 Jul 2014 00:24:00 +0200 blanchet stick to external proofs when invoking E, because they are more detailed and do not merge steps
Sat, 12 Jul 2014 11:31:23 +0200 blanchet don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
Tue, 24 Jun 2014 08:19:57 +0200 blanchet added 'dummy_thf_ml' prover for experiments with HOLyHammer
Tue, 17 Jun 2014 16:02:49 +0200 blanchet changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
Mon, 16 Jun 2014 19:41:01 +0200 blanchet use right delimiters for Waldmeister proofs
Mon, 16 Jun 2014 19:41:00 +0200 blanchet added 'waldmeister_new' as ATP
Mon, 16 Jun 2014 19:40:04 +0200 blanchet moved code around
Mon, 16 Jun 2014 19:39:41 +0200 blanchet give Z3 TPTP proofs a chance
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II.
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover
Mon, 19 May 2014 23:43:53 +0200 blanchet use E 1.8's auto scheduler option
Sun, 04 May 2014 18:14:59 +0200 blanchet added missing space between command-line options
Fri, 04 Apr 2014 15:56:40 +0200 blanchet use Z3 TPTP cores rather than proofs since the latter are somewhat broken
Fri, 04 Apr 2014 11:49:47 +0200 blanchet improved parsing of "z3_tptp" proofs
Thu, 03 Apr 2014 17:16:02 +0200 blanchet don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
Thu, 03 Apr 2014 17:00:14 +0200 blanchet use Alt-Ergo 0.95.2, the latest and greatest version
Thu, 03 Apr 2014 16:57:19 +0200 blanchet updated Z3 TPTP to 4.3.1+
Wed, 18 Dec 2013 16:50:14 +0100 blanchet made SML/NJ happier
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
Thu, 24 Oct 2013 12:43:33 +0200 blanchet use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation
Wed, 11 Sep 2013 09:50:48 +0200 blanchet adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)
Wed, 28 Aug 2013 18:44:50 +0200 blanchet got rid of old error -- users who install SPASS manually are responsible for any version mismatches
Tue, 13 Aug 2013 10:26:56 +0200 blanchet 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)
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
Sun, 26 May 2013 14:02:03 +0200 blanchet 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)
Tue, 21 May 2013 09:02:58 +0200 blanchet disabled choice in Satallax
Tue, 21 May 2013 09:02:58 +0200 blanchet prefer compiled version of LEO-II and Satallax if available
Tue, 21 May 2013 09:02:58 +0200 blanchet updated remote provers
Mon, 20 May 2013 11:27:13 +0200 blanchet started adding agsyHOL as an experimental prover
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of'
Wed, 08 May 2013 15:47:19 +0200 blanchet use right default for "uncurried_aliases" with polymorphic SPASS
Fri, 03 May 2013 10:27:24 +0200 blanchet tuning
Fri, 03 May 2013 10:26:34 +0200 blanchet pass certain readability-enhancing Vampire options only when an Isar proof is needed
Mon, 08 Apr 2013 12:11:06 +0200 blanchet robustness w.r.t. unknown arguments
Wed, 20 Mar 2013 15:35:35 +0100 blanchet use the right role for SPASS hypotheses
Tue, 05 Mar 2013 11:59:58 +0100 blanchet polymorphic SPASS is also SPASS
Thu, 21 Feb 2013 12:22:26 +0100 blanchet swap slices so that the last slice is more complete (for minimization)
Wed, 20 Feb 2013 15:26:19 +0100 blanchet upgraded to Alt-Ergo 0.95
Wed, 20 Feb 2013 10:45:01 +0100 blanchet turn off more evil Vampire options to facilitate Isar proof generation
Sun, 03 Feb 2013 17:31:33 +0100 blanchet tuned slicing (E-MaLeS and E-Par)
Sat, 02 Feb 2013 17:25:55 +0100 blanchet tune slices further
Sat, 02 Feb 2013 10:13:14 +0100 blanchet tweak ATP slices further
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned slices
Thu, 31 Jan 2013 17:54:05 +0100 blanchet store fact filter along with ATP slice
Thu, 17 Jan 2013 17:55:02 +0100 blanchet make SPASS more configurable, for experiments
Thu, 17 Jan 2013 14:01:45 +0100 blanchet added E-Par support
Mon, 03 Dec 2012 20:55:32 +0100 blanchet tweak SPASS default a tiny bit, so that a more interesting heuristic is chosen when "slicing=false" (for experiments)
Wed, 31 Oct 2012 11:23:21 +0100 blanchet less verbose -- the warning will reach the users anyway by other means
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuned messages
Wed, 31 Oct 2012 11:23:21 +0100 blanchet added a timeout around script that relies on the network
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuning
Tue, 14 Aug 2012 16:09:45 +0200 blanchet tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
less more (0) -300 -100 -60 tip