| Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
file |
diff |
annotate
|
| Fri, 23 Jul 2010 15:04:49 +0200 |
blanchet |
first step in using "fof" rather than "cnf" in TPTP problems
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 11:29:31 +0200 |
blanchet |
no polymorphic "var"s
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:47 +0200 |
blanchet |
rename "classrel" to "class_rel"
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:26 +0200 |
blanchet |
rename "combtyp" constructors
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:07 +0200 |
blanchet |
renamed "Literal" to "FOLLiteral"
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:13:46 +0200 |
blanchet |
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
|
file |
diff |
annotate
|
| Sat, 03 Jul 2010 00:49:12 +0200 |
blanchet |
remove needless signature entry
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 18:03:34 +0200 |
blanchet |
rewrote the TPTP problem generation code more or less from scratch;
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 13:23:13 +0200 |
blanchet |
rename functions
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:19:16 +0200 |
blanchet |
move "nice names" from Metis to TPTP format
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 17:32:28 +0200 |
blanchet |
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 17:08:39 +0200 |
blanchet |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:42:06 +0200 |
blanchet |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 16:28:12 +0200 |
blanchet |
fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 15:35:18 +0200 |
blanchet |
renamed for easier grep
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 23:54:02 +0200 |
blanchet |
factor out TPTP format output into file of its own, to facilitate further changes
|
file |
diff |
annotate
|