| Tue, 31 Jan 2012 14:39:21 +0100 |
blanchet |
new SPASS setup
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 12:43:48 +0100 |
blanchet |
distinguish between ":lr" and ":lt" (terminating) in DFG format
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 10:29:05 +0100 |
blanchet |
nicer keyword class avoidance scheme
|
file |
diff |
annotate
|
| 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
|