| 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 |