PRINT-PROOF-STRUCTURE is a top-level command.
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:


TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage