| Tue, 26 Jul 2011 14:53:00 +0200 |
further worked around LEO-II parser limitation, with eta-expansion
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
use syntactic sugar whenever possible in THF problems, to work around current LEO-II parser limitation (bang bang and query query are not handled correctly)
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
added option to control which lambda translation to use (for experiments)
|
file | diff | annotate |
| Thu, 14 Jul 2011 15:14:38 +0200 |
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 |
make SML/NJ happy + tuning
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
improved translation of lambdas in THF
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
added generation of lambdas in THF
|
file | diff | annotate |
| Tue, 05 Jul 2011 17:09:59 +0100 |
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 |
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 |
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 |
renamed ML function
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:35 +0200 |
improved ATP clausifier so it can deal with "x => (y <=> z)"
|
file | diff | annotate |
| Mon, 06 Jun 2011 20:36:34 +0200 |
killed odd connectives
|
file | diff | annotate |
| Wed, 01 Jun 2011 10:29:43 +0200 |
clausify "<=>" (needed for some type information)
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
proper handling of type variable classes in new Metis
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
more work on new metis that exploits the powerful new type encodings
|
file | diff | annotate |
| Tue, 31 May 2011 16:38:36 +0200 |
first step in sharing more code between ATP and Metis translation
|
file | diff | annotate |
| Fri, 27 May 2011 10:30:07 +0200 |
cleaner handling of equality and proxies (esp. for THF)
|
file | diff | annotate |
| Fri, 27 May 2011 10:30:07 +0200 |
fully support all type system encodings in typed formats (TFF, THF)
|
file | diff | annotate |
| Fri, 27 May 2011 10:30:07 +0200 |
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 |
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 |
more work on parsing LEO-II proofs and extracting uses of extensionality
|
file | diff | annotate |
| Tue, 24 May 2011 10:01:00 +0200 |
tuning
|
file | diff | annotate |
| Tue, 24 May 2011 10:00:38 +0200 |
more work on parsing LEO-II proofs without lambdas
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
identify HOL functions with THF functions
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
started adding support for THF output (but no lambdas)
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
eliminated more code duplication in Nitrox
|
file | diff | annotate |
| Sun, 22 May 2011 14:51:42 +0200 |
improved Waldmeister support -- even run it by default on unit equational goals
|
file | diff | annotate |
| Sun, 22 May 2011 14:51:04 +0200 |
removed SNARK hack now that SNARK is fixed
|
file | diff | annotate |
| Sun, 22 May 2011 14:51:01 +0200 |
added support for remote Waldmeister
|
file | diff | annotate |
| Sun, 22 May 2011 14:49:35 +0200 |
reorganized ATP formats a little bit
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:19 +0200 |
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 |
tuning
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:18 +0200 |
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
|
file | diff | annotate |
| Thu, 12 May 2011 15:29:18 +0200 |
renamed type systems for more consistency
|
file | diff | annotate |
| Fri, 06 May 2011 13:34:59 +0200 |
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 |
fixed long name truncation logic
|
file | diff | annotate |
| Mon, 02 May 2011 22:52:15 +0200 |
SNARK workaround
|
file | diff | annotate |
| Mon, 02 May 2011 22:52:15 +0200 |
proper default for TPTP source filed
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:25 +0200 |
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 |
avoid trailing digits for SNARK (type) names -- grr...
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:25 +0200 |
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 |
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 |
declare TFF types so that SNARK can be used with types
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
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 |
generate TFF type declarations in typed mode
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
added more rudimentary type support to Sledgehammer's ATP encoding
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
fixed type of ATP quantifier types (sic)
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
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 |
added support for TFF type declarations
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
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 |
added room for types in ATP quantifiers
|
file | diff | annotate |
| Sun, 01 May 2011 18:37:24 +0200 |
distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree
|
file | diff | annotate |
| Thu, 21 Apr 2011 22:18:28 +0200 |
detect some unsound proofs before showing them to the user
|
file | diff | annotate |
| Mon, 04 Apr 2011 18:53:35 +0200 |
if "monomorphize" is enabled, mangle the type information in the names by default
|
file | diff | annotate |
| Fri, 18 Feb 2011 12:32:55 +0100 |
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 |
eliminated Int.toString;
|
file | diff | annotate |
| Thu, 16 Sep 2010 11:59:45 +0200 |
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 |
factored out TSTP/SPASS/Vampire proof parsing;
|
file | diff | annotate |
| Wed, 15 Sep 2010 10:26:09 +0200 |
in debug mode, don't touch "$true" and "$false"
|
file | diff | annotate |