| 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
|