Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
better handling of individual type for DFG format (SPASS)
|
file |
diff |
annotate
|
Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
file |
diff |
annotate
|
Tue, 20 Dec 2011 18:59:50 +0100 |
blanchet |
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
|
file |
diff |
annotate
|
Tue, 20 Dec 2011 18:59:50 +0100 |
blanchet |
one more SPASS identifier
|
file |
diff |
annotate
|
Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
|
file |
diff |
annotate
|
Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
file |
diff |
annotate
|
Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
file |
diff |
annotate
|
Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
fixed THF type constructor syntax
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 18:13:36 +0200 |
blanchet |
added dummy polymorphic THF system
|
file |
diff |
annotate
|
Tue, 06 Sep 2011 09:11:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 14:43:20 +0200 |
blanchet |
use new syntax for Pi binder in TFF1 output
|
file |
diff |
annotate
|
Wed, 31 Aug 2011 08:49:10 +0200 |
blanchet |
fixed explicit declaration of TFF1 types
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:46 +0200 |
blanchet |
generate properly typed TFF1 (PFF) problems in the presence of type class predicates
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
added type abstractions (for declaring polymorphic constants) to TFF syntax
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:45 +0200 |
blanchet |
implement more of the polymorphic simply typed format TFF(1)
|
file |
diff |
annotate
|
Tue, 30 Aug 2011 16:07:34 +0200 |
blanchet |
first step towards polymorphic TFF + changed defaults for Vampire
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 23:38:09 +0200 |
blanchet |
make polymorphic encodings more complete
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 13:55:52 +0100 |
nik |
added choice operator output for
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning ATP problem output
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
clearer terminology
|
file |
diff |
annotate
|
Wed, 17 Aug 2011 10:03:58 +0200 |
blanchet |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file |
diff |
annotate
|
Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
further worked around LEO-II parser limitation, with eta-expansion
|
file |
diff |
annotate
|
Tue, 26 Jul 2011 14:53:00 +0200 |
blanchet |
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 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
file |
diff |
annotate
|
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
|