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:

<n>BUILD-PROOF-HIERARCHY

© 1988-99, Carnegie Mellon University.