| Thu, 09 Feb 2012 14:04:17 +0100 |
blanchet |
improved KBO weights -- beware of explicit applications
|
file |
diff |
annotate
|
| Thu, 09 Feb 2012 12:57:59 +0100 |
blanchet |
added possibility of generating KBO weights to DFG problems
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
improved hashing w.r.t. Mirabelle, to help debugging
|
file |
diff |
annotate
|
| Sat, 04 Feb 2012 12:08:18 +0100 |
blanchet |
tuned SPASS DFG output
|
file |
diff |
annotate
|
| Fri, 03 Feb 2012 18:00:55 +0100 |
blanchet |
extended SPASS/DFG output with ranks
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 01:55:17 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 01 Feb 2012 17:16:55 +0100 |
blanchet |
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 15:13:18 +0100 |
blanchet |
avoid name clash, really
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 15:10:03 +0100 |
blanchet |
fixed syntax bug in DFG output
|
file |
diff |
annotate
|
| 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
|