Download Tps3 Programmer`s Guide Peter B. Andrews Dan

1. DATA STRUCTURES
115
1.2. The Expansion Proof. In the mate toplevel, we have an expansion proof stored in the special variable current-eproof, which is an eproofstructure. current-eproof has a attribute etree, whose value is often used to
update variable current-topnode.
Actually, a whole formula is represented by a tree, each node of which
is an etree. At first, current-topnode is the root of the tree. Each node in
the tree can be one of the following structures, all of which are derived from
the structure etree, described above. We note only the differences between
these structures and etrees.
(1) econjunction is just an etree without any additional new attributes.
components is a list containing two elements, and junctive should
be dis or con.
(2) edisjunction is like econjunction.
(3) implication is like econjunction
(4) negation is just an etree. components contains one element and
junctive is neutral.
(5) skolem is an etree with two additional attributes:
(a) shallow: contains the shallow formula that the attribute skolem
represents. Never forget to make the corresponding changes in
it if you have changed some other parts of this node; otherwise
the proof cannot be transformed into natural deduction style
by etree-nat since the function get-shallow would not work normally.
(b) terms: is a skolem-term structure, containing a term replacing
the original variable, and something else.
(6) selection is also an etree with attributes shallow and terms, just as
skolem etree nodes. Whether the etree contains selection or skolem
nodes depends on the values of SKOLEM-DEFAULT.
(7) expansion is an etree with three additional properties:
(a) shallow: is the same as in skolem.
(b) terms: is an exp-var structure, containing the expansion variable for this expansion.
(c) prim-vars
(8) rewrite is an etree that rewrites the wff in some way. Rewrite nodes
have the following four additional attributes: shallow, justification,
ruleq-shallow, and reverse. The justification attribute is a symbol
which can currently be one of the following values (this list may not
be exhaustive):
(a) EQUIVWFFS: Usually means there have been some definition
expansions. In case dual instantiation is being used, it may
mean the wff has been rewritten to a conjunction or disjunction
of the wff and the instantiated form.
(b) LAMBDA, BETA, ETA: The wff is the result of the appropriate normalization.