blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42337
make new Skolemizer work also for "metisFT"
blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42336
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42335
experiment with definitional CNF
blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42334
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42333
try to repair out-of-sync situations in Metis
blanchet [Thu, 14 Apr 2011 11:24:04 +0200] rev 42332
handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
noschinl [Wed, 13 Apr 2011 21:38:00 +0200] rev 42331
Add YXML.parse_file to signature ...
noschinl [Wed, 13 Apr 2011 21:23:30 +0200] rev 42330
Add YXML.parse_file to parse and process big data files
noschinl [Wed, 13 Apr 2011 20:43:00 +0200] rev 42329
Generalized File.fold_lines to File.fold_fields
wenzelm [Mon, 11 Apr 2011 17:23:20 +0200] rev 42328
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;