| 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 11:29:31 +0200 |
blanchet |
move function
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:26:56 +0200 |
blanchet |
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:19:16 +0200 |
blanchet |
move "nice names" from Metis to TPTP format
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:05:37 +0200 |
blanchet |
move functions not needed by Metis out of "Metis_Clauses"
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 18:15:40 +0200 |
blanchet |
remove obsolete component of CNF clause tuple (and reorder it)
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 18:02:36 +0200 |
blanchet |
get rid of Skolem cache by performing CNF-conversion after fact selection
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 17:31:38 +0200 |
blanchet |
always perform relevance filtering on original formulas
|
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
| base
|