| Tue, 27 Jul 2010 19:41:19 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:17:15 +0200 |
blanchet |
standardize "Author" tags
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 18:38:10 +0200 |
blanchet |
get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 14:14:24 +0200 |
blanchet |
make TPTP generator accept full first-order formulas
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:21:25 +0200 |
blanchet |
renamed internal function
|
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
|
| Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
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 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
|