mengj [Fri, 18 Nov 2005 07:07:47 +0100] rev 18197
-- added combinator reduction axioms (typed and untyped) for HOL goals.
-- combined make_nnf functions for HOL and FOL goals.
-- hypothesis of goals are now also skolemized by inference.
mengj [Fri, 18 Nov 2005 07:07:06 +0100] rev 18196
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
mengj [Fri, 18 Nov 2005 07:06:07 +0100] rev 18195
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
mengj [Fri, 18 Nov 2005 07:05:11 +0100] rev 18194
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
-- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input.
-- added "check_is_fol" and "check_is_fol_term" into the signature.
wenzelm [Wed, 16 Nov 2005 19:34:19 +0100] rev 18193
tuned document;
wenzelm [Wed, 16 Nov 2005 17:50:35 +0100] rev 18192
tuned;
wenzelm [Wed, 16 Nov 2005 17:49:16 +0100] rev 18191
improved induction proof: local defs/fixes;