| Fri, 18 Nov 2005 07:10:37 +0100 |
mengj |
-- changed the interface of functions vampire_oracle and eprover_oracle.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:10:00 +0100 |
mengj |
-- terms are fully typed.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:54 +0100 |
mengj |
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:08:18 +0100 |
mengj |
-- 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.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:47 +0100 |
mengj |
-- added combinator reduction axioms (typed and untyped) for HOL goals.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:07:06 +0100 |
mengj |
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
|
changeset |
files
|
| Fri, 18 Nov 2005 07:06:07 +0100 |
mengj |
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
|
changeset |
files
|
| Fri, 18 Nov 2005 07:05:11 +0100 |
mengj |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
|
changeset |
files
|
| Wed, 16 Nov 2005 19:34:19 +0100 |
wenzelm |
tuned document;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:50:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:49:16 +0100 |
wenzelm |
improved induction proof: local defs/fixes;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:36 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:35 +0100 |
wenzelm |
added deskolem;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:34 +0100 |
wenzelm |
added THEN_ALL_NEW_CASES;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:33 +0100 |
wenzelm |
added revert_skolem, mk_def, add_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:32 +0100 |
wenzelm |
ProofContext.mk_def;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:31 +0100 |
wenzelm |
Term.betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:30 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:29 +0100 |
wenzelm |
added betapplys;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:28 +0100 |
wenzelm |
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:26 +0100 |
wenzelm |
norm_hhf: no normalization of protected props;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:25 +0100 |
wenzelm |
added protect_cong, cong_mono_thm;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:24 +0100 |
wenzelm |
induct: support local definitions to be passed through the induction;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:23 +0100 |
wenzelm |
Trueprop: use ObjectLogic.judgment etc.;
|
changeset |
files
|
| Wed, 16 Nov 2005 17:45:22 +0100 |
wenzelm |
Term.betapply;
|
changeset |
files
|
| Wed, 16 Nov 2005 15:29:23 +0100 |
paulson |
new version of "tryres" allowing multiple unifiers (apparently needed for
|
changeset |
files
|
| Wed, 16 Nov 2005 14:05:41 +0100 |
wenzelm |
pgmlsymbolson: append Symbol.xsymbolsN at end!
|
changeset |
files
|
| Tue, 15 Nov 2005 14:08:32 +0100 |
wenzelm |
better no -d option;
|
changeset |
files
|
| Tue, 15 Nov 2005 10:11:52 +0100 |
haftmann |
added generic transformators
|
changeset |
files
|