Thu, 14 Apr 2011 11:24:04 +0200 | blanchet | started clausifier examples | changeset | files |
Thu, 14 Apr 2011 11:24:04 +0200 | blanchet | make new Skolemizer work also for "metisFT" | changeset | files |
Thu, 14 Apr 2011 11:24:04 +0200 | blanchet | improve definitional CNF on goal by moving "not" past the quantifiers | changeset | files |