Fri, 18 Nov 2005 07:07:47 +0100 -- added combinator reduction axioms (typed and untyped) for HOL goals.
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.
Fri, 18 Nov 2005 07:07:06 +0100 -- 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: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).
Fri, 18 Nov 2005 07:06:07 +0100 -- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
mengj [Fri, 18 Nov 2005 07:06:07 +0100] rev 18195
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
Fri, 18 Nov 2005 07:05:11 +0100 -- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
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.
Wed, 16 Nov 2005 19:34:19 +0100 tuned document;
wenzelm [Wed, 16 Nov 2005 19:34:19 +0100] rev 18193
tuned document;
Wed, 16 Nov 2005 17:50:35 +0100 tuned;
wenzelm [Wed, 16 Nov 2005 17:50:35 +0100] rev 18192
tuned;
Wed, 16 Nov 2005 17:49:16 +0100 improved induction proof: local defs/fixes;
wenzelm [Wed, 16 Nov 2005 17:49:16 +0100] rev 18191
improved induction proof: local defs/fixes;
Wed, 16 Nov 2005 17:45:36 +0100 tuned Pattern.match/unify;
wenzelm [Wed, 16 Nov 2005 17:45:36 +0100] rev 18190
tuned Pattern.match/unify; tuned fold;
Wed, 16 Nov 2005 17:45:35 +0100 added deskolem;
wenzelm [Wed, 16 Nov 2005 17:45:35 +0100] rev 18189
added deskolem;
Wed, 16 Nov 2005 17:45:34 +0100 added THEN_ALL_NEW_CASES;
wenzelm [Wed, 16 Nov 2005 17:45:34 +0100] rev 18188
added THEN_ALL_NEW_CASES; Syntax.deskolem;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip