Mon, 26 Jul 2010 17:22:39 +0200 | blanchet | remove more Skolemization-aware code | changeset | files |
Mon, 26 Jul 2010 17:17:59 +0200 | blanchet | kill Skolem handling in Sledgehammer | changeset | files |
Mon, 26 Jul 2010 17:09:10 +0200 | blanchet | simplify "conjecture_shape" business, as a result of using FOF instead of CNF | changeset | files |
Mon, 26 Jul 2010 17:03:21 +0200 | blanchet | generate full first-order formulas (FOF) in Sledgehammer | changeset | files |
Mon, 26 Jul 2010 14:14:24 +0200 | blanchet | make TPTP generator accept full first-order formulas | changeset | files |
Mon, 26 Jul 2010 11:26:47 +0200 | blanchet | generate close formulas for SPASS, but not for the others (to avoid clutter) | changeset | files |