Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_systems.ML
Tue, 24 May 2011 00:01:33 +0200 blanchet clearer SystemOnTPTP errors file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet give fewer equations to Waldmeister file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet detect inappropriate problems and crashes better in Waldmeister file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals file | diff | annotate
Sun, 22 May 2011 14:51:41 +0200 blanchet fish out axioms in Waldmeister output file | diff | annotate
Sun, 22 May 2011 14:51:04 +0200 blanchet recognize one more SystemOnTPTP error file | diff | annotate
Sun, 22 May 2011 14:51:01 +0200 blanchet added support for remote Waldmeister file | diff | annotate
Sun, 22 May 2011 14:50:32 +0200 blanchet added Waldmeister file | diff | annotate
Sun, 22 May 2011 14:49:35 +0200 blanchet reorganized ATP formats a little bit file | diff | annotate
Fri, 20 May 2011 12:47:59 +0200 blanchet make sure the Vampire incomplete proof detection code kicks in file | diff | annotate
Thu, 19 May 2011 10:24:13 +0200 blanchet renamed "simple_types" to "simple" file | diff | annotate
Thu, 19 May 2011 10:24:13 +0200 blanchet tweaked ATP type systems further based on Judgment Day file | diff | annotate
Thu, 19 May 2011 10:24:13 +0200 blanchet better error reporting: detect missing E proofs and remove Vampire native format error file | diff | annotate
Fri, 13 May 2011 10:10:43 +0200 blanchet tweak E slices file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet allow each slice to have its own type system file | diff | annotate
Fri, 06 May 2011 13:35:00 +0200 blanchet further improved type system setup based on Judgment Days file | diff | annotate
Fri, 06 May 2011 13:34:59 +0200 blanchet allow each prover to specify its own formula kind for symbols occurring in the conjecture file | diff | annotate
Fri, 06 May 2011 13:34:59 +0200 blanchet better type system setup, based on Judgment Day file | diff | annotate
Thu, 05 May 2011 09:43:39 +0200 blanchet improve suggested type system list based on evaluation file | diff | annotate
Wed, 04 May 2011 22:56:33 +0200 blanchet renamed "many_typed" to "simple" (as in simple types) file | diff | annotate
Wed, 04 May 2011 22:47:13 +0200 blanchet added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types) file | diff | annotate
Tue, 03 May 2011 08:52:32 +0200 blanchet whitespace tuning file | diff | annotate
Tue, 03 May 2011 00:10:22 +0200 blanchet replaced some Unsynchronized.refs with Config.Ts file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet better default type systems for SNARK and ToFoF file | diff | annotate
Mon, 02 May 2011 14:40:57 +0200 blanchet use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used file | diff | annotate
Mon, 02 May 2011 14:22:34 +0200 blanchet supply type-system defaults for major ATPs file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet pick up GaveUp error on SystemOnTPTP file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet define type system in ATP module so that ATPs can suggest a type system file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet recognize more SystemOnTPTP errors file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet better known failure recognition for ToFoF-E file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format file | diff | annotate
Sun, 01 May 2011 18:37:23 +0200 blanchet get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet implemented general slicing for ATPs, especially E 1.2w and above file | diff | annotate
Thu, 14 Apr 2011 11:24:04 +0200 blanchet handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used file | diff | annotate
Fri, 18 Feb 2011 15:17:39 +0100 blanchet adjust fudge factors file | diff | annotate
Fri, 18 Feb 2011 12:32:55 +0100 blanchet extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs file | diff | annotate
Tue, 15 Feb 2011 18:32:58 +0100 blanchet make experimental "Z3 ATP" work on Linux as well file | diff | annotate
Tue, 15 Feb 2011 10:03:10 +0100 blanchet adjusted fudge factors (based on Judgment Day runs) file | diff | annotate
Thu, 10 Feb 2011 10:09:38 +0100 blanchet make minimizer verbose file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices) file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet renamed field file | diff | annotate
Wed, 09 Feb 2011 17:18:58 +0100 blanchet added "Z3 as an ATP" support to Sledgehammer locally file | diff | annotate
Wed, 09 Feb 2011 17:18:57 +0100 blanchet added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation file | diff | annotate
Tue, 08 Feb 2011 16:10:10 +0100 blanchet available_provers ~> supported_provers (for clarity) file | diff | annotate
Tue, 08 Feb 2011 16:10:08 +0100 blanchet added support for bleeding-edge E weighting function "SymOffsetsWeight" file | diff | annotate
Tue, 21 Dec 2010 03:56:51 +0100 blanchet added "smt_triggers" option to experiment with triggers in Sledgehammer; file | diff | annotate
Tue, 21 Dec 2010 01:12:17 +0100 blanchet enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day file | diff | annotate
Mon, 20 Dec 2010 14:17:49 +0100 blanchet disable feature that was enabled by mistake file | diff | annotate
Mon, 20 Dec 2010 13:52:44 +0100 blanchet use the options provided by Stephan Schulz -- much better file | diff | annotate
Mon, 20 Dec 2010 12:12:35 +0100 blanchet optionally supply constant weights to E -- turned off by default until properly parameterized file | diff | annotate
Sat, 18 Dec 2010 14:02:14 +0100 blanchet tuning file | diff | annotate
Fri, 17 Dec 2010 12:01:49 +0100 blanchet fewer facts to SInE-E file | diff | annotate
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) file | diff | annotate
less more (0) -100 -60 tip
isabelle