Browsing Proofs

There are also Print Forms for Proofs .

The various links pertaining to a proof are accessed from its inference step pages.

In Nuprl, proofs are trees of assertions, each assertion being a sequence of assumptions and variable declarations together with a conclusion. Each node is considered as a goal whose subgoals are its children; a goal follows from its subgoals. The subgoals are generated from the goal by a justification called a "tactic" which is an executable explanation of how to justify the inference to the goal from the subgoals by means of various primitive inference rules.

A goal with an empty list of subgoals is completely proved. ( Example )

A proof object in Nuprl will be a proof tree whose topmost goal has no assumptions or variable declarations.

Proof objects are typically referred to by a citation of the main goal along with a link to the proof top. Normally, citations of lemmas in the justification of an inference are presented this way. ( Example )

Interactive examination of proofs must for now proceed one inference step at a time. Each page containing an inference step includes:

The goal.
The numbered subgoals.
The tactic justifying the inference.
The name of the object containing the inference step.
The address of the inference step within the whole proof tree.

The address is a list of integers, and each numeral in the address is presented as a link to the node with the appropriate address, which makes it easier to jump up to a higher node in the tree.

The subgoals of an inference are numbered, and if the proof of the subgoal is non-trivial, then the numeral is presented as a link to the inference having the subgoal as its goal. This is how you walk down the proof tree. ( Example -- the proof of subgoal 2 is considered trivial, and so is not accessible.)

To save space and ease reading, when an initial segment of the hypotheses and declarations is inherited from the goal, they are elided in the subgoal. If you follow the link into the subproof, the elided elements are restored in the goal of the subproof. ( Example )