src/HOL/Tools/ATP/atp_systems.ML
Tue, 07 Aug 2012 22:54:27 +0200 blanchet proper quoting
Tue, 07 Aug 2012 14:29:18 +0200 blanchet stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
Tue, 07 Aug 2012 13:03:50 +0200 blanchet specify full path to clausifier
Mon, 06 Aug 2012 22:12:17 +0200 blanchet added iProver(-Eq) local
Thu, 02 Aug 2012 10:10:29 +0200 blanchet support older versions of Vampire
Thu, 02 Aug 2012 10:10:29 +0200 blanchet added E-MaLeS to list of provers for testing
Fri, 27 Jul 2012 17:34:33 +0200 blanchet tweaks in preparation for type encoding evaluation
Fri, 27 Jul 2012 08:52:40 +0200 blanchet extract Z3 unsat cores (for "z3_tptp")
Fri, 20 Jul 2012 22:19:45 +0200 blanchet use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
Tue, 10 Jul 2012 23:36:03 +0200 blanchet don't ask E to generate a detailed proofs if not needed
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output
Tue, 26 Jun 2012 11:14:39 +0200 blanchet tuning
Tue, 26 Jun 2012 11:14:39 +0200 blanchet removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
Wed, 06 Jun 2012 10:35:05 +0200 blanchet pass more facts to LEO-II, in the light of latest evaluation
Wed, 06 Jun 2012 10:35:05 +0200 blanchet robust LEO-II setup that doesn't rely on ".leoatprc"
Wed, 06 Jun 2012 10:35:05 +0200 blanchet tweaked remote Vampire version
Mon, 28 May 2012 20:51:23 +0200 blanchet tweaked remote Vampire setup
Mon, 28 May 2012 20:45:28 +0200 blanchet killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
Mon, 28 May 2012 20:25:38 +0200 blanchet don't generate definitions for LEO-II -- this cuases more harm than good
Thu, 24 May 2012 15:11:53 +0200 blanchet update Satallax setup based on evaluation
Thu, 24 May 2012 15:01:29 +0200 blanchet gracefully handle definition-looking premises
Wed, 23 May 2012 21:19:48 +0200 blanchet tuned names
Wed, 23 May 2012 21:19:48 +0200 blanchet improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
Wed, 23 May 2012 21:19:48 +0200 blanchet better handling of incomplete TSTP proofs
Wed, 23 May 2012 13:28:20 +0200 blanchet lower the monomorphization thresholds for less scalable provers
Tue, 22 May 2012 16:59:27 +0200 blanchet added one slice with configurable simplification turned off
Mon, 21 May 2012 11:31:52 +0200 blanchet invite users to upgrade their SPASS (so we can get rid of old code)
Mon, 21 May 2012 11:31:52 +0200 blanchet start phasing out old SPASS
Mon, 21 May 2012 11:31:52 +0200 blanchet minor tweak in Vampire setup
Wed, 16 May 2012 18:16:51 +0200 blanchet minor slice tweaking (swapped two slices to move polymorphic encoding up a bit)
Mon, 14 May 2012 15:54:26 +0200 blanchet tuning
Sun, 13 May 2012 16:31:01 +0200 blanchet LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
Sun, 13 May 2012 16:31:01 +0200 blanchet get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
Thu, 10 May 2012 10:07:41 +0200 blanchet pass fewer facts to LEO-II and Satallax
Thu, 10 May 2012 10:07:40 +0200 blanchet tweak LEO-II setup
Thu, 10 May 2012 10:07:40 +0200 blanchet use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
Fri, 27 Apr 2012 13:18:55 +0200 blanchet tweak LEO-II setup
Thu, 26 Apr 2012 00:29:46 +0200 blanchet tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)
Tue, 24 Apr 2012 20:55:09 +0200 blanchet removed confusing error
Sun, 22 Apr 2012 14:16:46 +0200 blanchet tried harder to make SML/NJ happy
Sat, 21 Apr 2012 11:15:49 +0200 blanchet tried to make SML/NJ happy
Thu, 19 Apr 2012 17:49:08 +0200 blanchet true delayed evaluation of "SPASS_VERSION" environment variable
Tue, 17 Apr 2012 13:54:31 +0200 blanchet more helpful error message
Tue, 17 Apr 2012 13:54:31 +0200 blanchet avoid option introduced in E 1.2 when invoking older versions of E
Mon, 16 Apr 2012 23:07:40 +0200 wenzelm redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
Tue, 27 Mar 2012 16:59:13 +0300 blanchet tweak slices, based on eval by Daniel Wand
Wed, 21 Mar 2012 16:53:24 +0100 blanchet removed Satallax option, now that this is the default
Wed, 21 Mar 2012 16:53:24 +0100 blanchet improve "remote_satallax" by exploiting unsat core
Wed, 21 Mar 2012 16:53:24 +0100 blanchet generate weights and precedences for predicates as well
Tue, 20 Mar 2012 18:42:45 +0100 blanchet made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
Tue, 20 Mar 2012 18:42:45 +0100 blanchet tweaks
Tue, 20 Mar 2012 13:53:09 +0100 blanchet added term_order option to Mirabelle
Tue, 20 Mar 2012 10:06:35 +0100 blanchet added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
Tue, 20 Mar 2012 00:44:30 +0100 blanchet continued implementation of term ordering attributes
Tue, 20 Mar 2012 00:44:30 +0100 blanchet implement term order attribute (for experiments)
Tue, 20 Mar 2012 00:44:30 +0100 blanchet tuning -- don't refer to old, internal version number (needlessly confusing now)
Tue, 20 Mar 2012 00:44:30 +0100 blanchet more weight attribute tuning
Tue, 20 Mar 2012 00:44:30 +0100 blanchet 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
Tue, 20 Mar 2012 00:44:30 +0100 blanchet internal renamings
Tue, 20 Mar 2012 00:44:30 +0100 blanchet renamed E weight attribute
less more (0) -100 -60 tip