The precursor of Mark2 was EFTTP (*EFT* Theorem Prover) which
had certain points of resemblance to Mark2 along with notable
differences.

The notation of EFTTP followed the term structure of *EFT*
exactly, with the addition of special term constructors for FUNCTORS
(operations on Functions, the third sort) and the attachment of
embedded theorems. The notation of EFTTP was very awkward; it did not
support infix notation at all, for example (the current `?x + ?y`
would be `+[x?,y?]` under EFTTP).

The avoidance of bound variables was made practical by the direct
implementation of the Abstraction Theorem of the preceding section as
a tactic. Parameterized tactics were not at that time available, but
I will describe the `ABSTRACT` tactic in its modern form, as it
appears in Mark2, rather than delving into the peculiar expedients of
EFTTP. The tactic is invoked in the following format `(ABSTRACT @
term1) => term2`, and execution of the tactic yields a term `
function_term @ term1`, in which, if `term2` can be expressed as
a function of `term1` under appropriate constraints (such as
stratification; obviously a different abstraction theorem is being
implemented than in EFTTP!), the term `function_term` will not
depend on `term1`. Moreover, as noted above, both in EFTTP and in
Mark2, the algorithm implemented by `ABSTRACT` produces more or
less readable terms parallel in structure to the terms from which they
are abstracted, though not as readable as conventional
-terms. The implementation of `ABSTRACT` is a subject
for the section on programming style (NOTE TO BE REMOVED: be sure to
note there why `RAISE` is needed; the problem of abstraction
from operators). A tactic `REDUCE`, which needs no parameter,
undoes the effect of `ABSTRACT`. The two tactics together allowed
the automation of operations of global substitution under the prover,
which made it possible to go quite far without any use of bound
variables.

The Cond[(*x*,*y*),(*z*,*w*)] construct of *EFT* allows the
construction of case expressions. The analogous construction under
Mark2 is `(?x = ?y) || (?z , ?w)` (the second set of parentheses
would normally not appear). All reasoning under hypotheses is managed
in EFTTP or Mark2 as equational reasoning about case expressions. The
axioms (DIST) and especially (HYP) manage the system of hypothetical
reasoning of *EFT*, which is adequate to the demands of
propositional logic. In fact, a complete tautology checking tactic
has been developed from the *EFT* axioms under both provers.
Abstraction and reduction play an important role in the development of
tactics which support this style of reasoning efficiently; the
substitutions for arguments of functions in the axioms (DIST) and
(HYP) can be converted to global substitutions in expressions of
arbitrary form by the use of abstraction followed by reduction (the
user never sees an abstraction term).

Reasoning about case expressions is implemented in a ``hard-wired'' way in the new hypothesis facility (see above).

The paper from which the description of the *EFT* logic in the
previous subsection is drawn proves that *EFT* theories are
precisely equivalent to first-order theories with infinite domain (the
pairing forces the infinite domain).

The axiom (HILBERT) introduces an operator analogous to the Hilbert epsilon operator for defining quantifiers (HOL has a similar approach to defining quantifiers). A choice operator could be used in a similar way in Mark2's logic; if it is desired that the Axiom of Choice not be assumed, this can be made possible by declaring the choice operator as ``opaque'' to abstraction.

Fri Sep 5 16:28:58 MDT 1997