Fri, 18 Nov 2005 07:10:37 +0100 -- changed the interface of functions vampire_oracle and eprover_oracle.
mengj [Fri, 18 Nov 2005 07:10:37 +0100] rev 18201
-- changed the interface of functions vampire_oracle and eprover_oracle.
Fri, 18 Nov 2005 07:10:00 +0100 -- terms are fully typed.
mengj [Fri, 18 Nov 2005 07:10:00 +0100] rev 18200
-- terms are fully typed. -- only the top-level boolean terms are predicates.
Fri, 18 Nov 2005 07:08:54 +0100 -- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
mengj [Fri, 18 Nov 2005 07:08:54 +0100] rev 18199
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
Fri, 18 Nov 2005 07:08:18 +0100 -- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj [Fri, 18 Nov 2005 07:08:18 +0100] rev 18198
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
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;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip