This prints the structure of the proof outline. The

structure is generated by BUILD-PROOF-HIERARCHY. Linear chains

of line numbers are printed which indicate the logical chains of

inferences. Each link in a linear chain is indicated by an

arrow (l1)->(l2) where l1 and l2 are line numbers. If line l2

does not follow in a single step from l1 (i.e., by a single application

of an inference rules), then PRINT-PROOF-STRUCTURE will also show the

linear chains of inference used to justify (l1)->(l2). Some lines

(such as those without hypotheses and planned lines) are

exceptions. These top level lines are sometimes printed alone

(instead of in arrow notation). This could be read TRUE->(l)

to maintain consistent notation, but the notation (l) appears

more readable in practice.

The command format for PRINT-PROOF-STRUCTURE is:

<n>PRINT-PROOF-STRUCTURE

© 1988-99, Carnegie Mellon University.