BUILD-PROOF-HIERARCHY : MEXPRBUILD-PROOF-HIERARCHY is a top-level command.
This command builds hierarchical information into the proof outline.
The information includes associations between lines and linear chains
of inferences which trace the consequences of the most recent hypothesis
of a line. That is, a line
ln) Hn,m |- an
would be associated with a linear chain of lines l1,...,ln
where m is the line corresponding to the most recent hypothesis and
the proof would justify the modified lines
l1) H1,m |- l1
l2) H2,l1 |- l2
l3) H3,l2 |- l3
. . .
ln) Hn,ln-1 |- ln
where H1 < H2 < . . . < Hn (subset relation).
That is, we trace the consequences of the hypothesis m to the
consequence ln. Such a linear chain is on one level of the hierarchy.
One level down on the hierarchy would be the linear chains associated
with each of the lines used to justify l1,...,ln (except those which
appear in the chain l1,...,ln). If the proof is complete,
then lines l1 and m will be the same.
Lines without hypotheses are also associated with such
"linear chains", following the rule that l1 < l2 if
the proof justifies the inference l1 |- l2.
The resulting hierarchy information is used by PBRIEF, EXPLAIN,
and PRINT-PROOF-STRUCTURE to help users focus on the logical
structure of a proof.
The command format for BUILD-PROOF-HIERARCHY is:
TPS documentation homepage