Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_problem.ML
Thu, 14 Jul 2011 15:14:38 +0200 blanchet don't generate Waldmeister problems with only a conjecture, since it makes it crash sometimes file | diff | annotate
Wed, 06 Jul 2011 17:19:34 +0100 blanchet make SML/NJ happy + tuning file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik improved translation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik added generation of lambdas in THF file | diff | annotate
Tue, 05 Jul 2011 17:09:59 +0100 nik add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) file | diff | annotate
Thu, 16 Jun 2011 13:50:35 +0200 blanchet added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users file | diff | annotate
Wed, 08 Jun 2011 16:20:19 +0200 blanchet pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types file | diff | annotate
Tue, 07 Jun 2011 07:06:24 +0200 blanchet renamed ML function file | diff | annotate
Mon, 06 Jun 2011 20:36:35 +0200 blanchet improved ATP clausifier so it can deal with "x => (y <=> z)" file | diff | annotate
Mon, 06 Jun 2011 20:36:34 +0200 blanchet killed odd connectives file | diff | annotate
Wed, 01 Jun 2011 10:29:43 +0200 blanchet clausify "<=>" (needed for some type information) file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet proper handling of type variable classes in new Metis file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet more work on new metis that exploits the powerful new type encodings file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet cleaner handling of equality and proxies (esp. for THF) file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet fully support all type system encodings in typed formats (TFF, THF) file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments) file | diff | annotate
Tue, 24 May 2011 18:04:23 +0200 blanchet ensure that the argument of logical negation is enclosed in parentheses in THF mode file | diff | annotate
Tue, 24 May 2011 10:01:03 +0200 blanchet more work on parsing LEO-II proofs and extracting uses of extensionality file | diff | annotate
Tue, 24 May 2011 10:01:00 +0200 blanchet tuning file | diff | annotate
Tue, 24 May 2011 10:00:38 +0200 blanchet more work on parsing LEO-II proofs without lambdas file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet identify HOL functions with THF functions file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet started adding support for THF output (but no lambdas) file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet eliminated more code duplication in Nitrox 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:04 +0200 blanchet removed SNARK hack now that SNARK is fixed 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:49:35 +0200 blanchet reorganized ATP formats a little bit file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet tuning file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option file | diff | annotate
Thu, 12 May 2011 15:29:18 +0200 blanchet renamed type systems for more consistency 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
Tue, 03 May 2011 18:47:22 +0200 blanchet fixed long name truncation logic file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet SNARK workaround file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet proper default for TPTP source filed 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 avoid trailing digits for SNARK (type) names -- grr... 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:24 +0200 blanchet shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet declare TFF types so that SNARK can be used with types file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas) file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet generate TFF type declarations in typed mode file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added more rudimentary type support to Sledgehammer's ATP encoding file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet fixed type of ATP quantifier types (sic) file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added support for TFF type declarations file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet added room for types in ATP quantifiers file | diff | annotate
Sun, 01 May 2011 18:37:24 +0200 blanchet distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree 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
Mon, 04 Apr 2011 18:53:35 +0200 blanchet if "monomorphize" is enabled, mangle the type information in the names by default 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
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString; file | diff | annotate
Thu, 16 Sep 2010 11:59:45 +0200 blanchet use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs file | diff | annotate
Thu, 16 Sep 2010 11:12:08 +0200 blanchet factored out TSTP/SPASS/Vampire proof parsing; file | diff | annotate
Wed, 15 Sep 2010 10:26:09 +0200 blanchet in debug mode, don't touch "$true" and "$false" file | diff | annotate
Thu, 02 Sep 2010 22:49:56 +0200 blanchet fix bug in "debug" mode file | diff | annotate
Sun, 22 Aug 2010 09:43:10 +0200 blanchet prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; file | diff | annotate
Fri, 20 Aug 2010 15:16:27 +0200 blanchet use "hypothesis" rather than "conjecture" for hypotheses in TPTP format; file | diff | annotate
less more (0) -60 tip
isabelle