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
|
Tue, 17 Aug 2010 16:46:43 +0200 |
blanchet |
more parentheses in TPTP formulas, just in case
|
file |
diff |
annotate
|
Thu, 29 Jul 2010 16:11:02 +0200 |
blanchet |
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 19:04:59 +0200 |
blanchet |
consequence of directory renaming
|
file |
diff |
annotate
|
Wed, 28 Jul 2010 19:01:34 +0200 |
blanchet |
rename directory
|
file |
diff |
annotate
| base
|