next up previous contents index
Next: The Form of Up: The Rules Previous: Typehood and Membership

The Rules

The     Nuprl system has been designed to accommodate the top--down  construction of proofs by refinement. In this style one proves a judgement (i.e., a goal) by applying a refinement  rule, thereby obtaining a set of judgements called subgoals, and then proving each of the subgoals. The mechanics of using the proof--editing system were discussed in chapter 7. In this section we will describe the refinement rules themselves. First we give some general comments regarding the rules and then proceed to give a description of each rule.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995