src/HOL/Tools/ATP/atp_systems.ML
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
Fri, 24 Feb 2012 11:23:35 +0100 blanchet added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
Tue, 14 Feb 2012 20:13:07 +0100 blanchet don't report spurious LEO-II errors
Tue, 14 Feb 2012 18:58:33 +0100 blanchet better error message
Sat, 11 Feb 2012 13:41:36 +0100 blanchet new SPASS options
Fri, 10 Feb 2012 16:33:58 +0100 blanchet update SPASS slices
Thu, 09 Feb 2012 14:35:27 +0100 blanchet new SPASS slices
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding
Sun, 05 Feb 2012 13:28:51 +0100 blanchet remove option that's on by default
Sun, 05 Feb 2012 12:27:10 +0100 blanchet no need for a script/mega-hack with the new SPASS
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing
Sat, 04 Feb 2012 12:08:18 +0100 blanchet made option available to users (mostly for experiments)
Fri, 03 Feb 2012 18:00:55 +0100 blanchet optimization: slice caching in case two consecutive slices are nearly identical
Thu, 02 Feb 2012 15:14:18 +0100 blanchet change 9ce354a77908 wasn't quite right -- here's an improvement
Thu, 02 Feb 2012 12:51:03 +0100 blanchet better SPASS setup
Thu, 02 Feb 2012 12:42:05 +0100 blanchet include new SPASS by default if available
Tue, 31 Jan 2012 17:09:08 +0100 blanchet third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
Tue, 31 Jan 2012 16:11:15 +0100 blanchet improve SPASS setup
Tue, 31 Jan 2012 15:10:03 +0100 blanchet fixed syntax bug in DFG output
Tue, 31 Jan 2012 14:39:21 +0100 blanchet new SPASS setup
Mon, 30 Jan 2012 17:18:58 +0100 blanchet new SPASS setup
Mon, 30 Jan 2012 17:15:59 +0100 blanchet rename lambda translation schemes
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file
Wed, 14 Dec 2011 18:07:32 +0100 blanchet SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
Wed, 16 Nov 2011 17:06:14 +0100 blanchet give each time slice its own lambda translation
Sun, 06 Nov 2011 11:16:37 +0100 blanchet renamed experimental systems
Fri, 04 Nov 2011 15:05:59 +0000 blanchet document new experimental provers
Fri, 04 Nov 2011 15:05:58 +0000 blanchet added remote iProver(-Eq) for experimentation
Sat, 29 Oct 2011 13:15:58 +0200 blanchet 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
less more (0) -100 -60 tip