next up previous contents
Next: The Logical Preamble Up: Logical Style Previous: The Logic of an

Implementation of EFT

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.

next up previous contents
Next: The Logical Preamble Up: Logical Style Previous: The Logic of an

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997