src/HOL/Tools/ATP/atp_systems.ML
Sat, 18 Dec 2010 14:02:14 +0100 blanchet tuning
Fri, 17 Dec 2010 12:01:49 +0100 blanchet fewer facts to SInE-E
Thu, 16 Dec 2010 15:12:17 +0100 blanchet fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
Wed, 15 Dec 2010 11:26:29 +0100 blanchet added timeout max for remote server invocation
Tue, 23 Nov 2010 22:37:16 +0100 blanchet more precise error handling for Z3;
Thu, 18 Nov 2010 10:52:38 +0100 blanchet remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
Mon, 08 Nov 2010 09:10:44 +0100 blanchet recognize Vampire error
Wed, 03 Nov 2010 23:01:30 +0100 blanchet give E one more second, to prevent cases where it finds a proof but has no time to print it
Thu, 21 Oct 2010 16:25:40 +0200 blanchet first step in adding support for an SMT backend to Sledgehammer
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
Thu, 16 Sep 2010 15:16:08 +0200 blanchet refactoring: move ATP proof and error extraction code to "ATP_Proof" module
Tue, 14 Sep 2010 23:37:34 +0200 blanchet prefer version 0.6 of Vampire, now that we can parse its output
Sat, 11 Sep 2010 12:30:50 +0200 blanchet tuning
Sat, 11 Sep 2010 10:22:52 +0200 blanchet change order of default ATPs;
Thu, 09 Sep 2010 16:27:36 +0200 blanchet more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
Thu, 09 Sep 2010 16:06:11 +0200 blanchet better error reporting when the Sledgehammer minimizer is interrupted
Wed, 08 Sep 2010 19:20:52 +0200 blanchet improve SInE-E failure message
Thu, 02 Sep 2010 00:17:56 +0200 blanchet SNARK doesn't like facts
Thu, 02 Sep 2010 00:15:53 +0200 blanchet show real CPU time
Wed, 01 Sep 2010 22:31:45 +0200 blanchet add dependency of "spass" script
Wed, 01 Sep 2010 18:42:31 +0200 blanchet lower number of facts given to SInE
Wed, 01 Sep 2010 17:27:10 +0200 blanchet got rid of the "theory_relevant" option;
Thu, 26 Aug 2010 13:55:30 +0200 blanchet fix Vampire version numbers
Wed, 25 Aug 2010 17:49:52 +0200 blanchet make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
Wed, 25 Aug 2010 09:05:22 +0200 blanchet make SML/NJ happy
Tue, 24 Aug 2010 21:40:03 +0200 blanchet better workaround for E's off-by-one-second issue
Tue, 24 Aug 2010 15:06:47 +0200 blanchet use a soft time limit for E
Tue, 24 Aug 2010 14:36:29 +0200 blanchet make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
Mon, 23 Aug 2010 21:11:30 +0200 blanchet adjust fudge factors in the light of experiments
Mon, 23 Aug 2010 17:53:49 +0200 blanchet revert unintended change
Mon, 23 Aug 2010 16:12:41 +0200 blanchet prevent double inclusion of the fact "True_or_False" in TPTP problems
Mon, 23 Aug 2010 09:04:37 +0200 blanchet play with fudge factor + parse one more Vampire error
Mon, 23 Aug 2010 00:09:25 +0200 blanchet fiddle a bit with the SPASS fudge number
Sun, 22 Aug 2010 22:47:03 +0200 blanchet be more generous towards SPASS's -SOS mode
Sun, 22 Aug 2010 09:43:10 +0200 blanchet prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible;
Thu, 19 Aug 2010 13:04:37 +0200 blanchet fix SInE's error handling + run "vampire" locally if either SPASS or E is missing
Thu, 19 Aug 2010 11:29:53 +0200 blanchet added remote SInE and remote SNARK
Wed, 18 Aug 2010 20:53:55 +0200 blanchet don't get confused by wrong slice
Wed, 18 Aug 2010 17:09:05 +0200 blanchet added "max_relevant_per_iter" option to Sledgehammer
Wed, 18 Aug 2010 16:42:37 +0200 blanchet thank Andrei instead of Tanya
Wed, 18 Aug 2010 12:04:00 +0200 blanchet rename enum values
Tue, 17 Aug 2010 18:14:50 +0200 blanchet tweaking
Tue, 17 Aug 2010 17:01:31 +0200 blanchet merged
Tue, 17 Aug 2010 14:35:44 +0200 blanchet improve detection of old Vampire versions
Tue, 17 Aug 2010 16:47:19 +0200 wenzelm made 9043eefe8d71 actually compile;
Mon, 16 Aug 2010 13:59:04 +0200 blanchet detect old Vampire and give a nicer error message
Mon, 16 Aug 2010 09:39:05 +0200 blanchet Geoff's formatter now needs closed formulas
Mon, 09 Aug 2010 11:05:45 +0200 blanchet fiddle some more with "max_new_relevant_facts_per_iter"
Thu, 29 Jul 2010 20:02:02 +0200 blanchet avoid "ATP Error: Error: blah" style messages
Thu, 29 Jul 2010 19:26:42 +0200 blanchet better error and minimizer output
Thu, 29 Jul 2010 18:45:41 +0200 blanchet speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
Thu, 29 Jul 2010 16:54:46 +0200 blanchet fiddle with the fudge factors, to get similar results as before
Thu, 29 Jul 2010 09:41:49 +0200 blanchet improved ATP error handling some more
Thu, 29 Jul 2010 00:28:57 +0200 blanchet shorter URL
Wed, 28 Jul 2010 23:01:27 +0200 blanchet handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
Wed, 28 Jul 2010 19:23:56 +0200 blanchet renamed environment variable
Wed, 28 Jul 2010 19:04:59 +0200 blanchet consequence of directory renaming
Wed, 28 Jul 2010 19:01:34 +0200 blanchet rename directory
less more (0) tip