next up previous contents index
Next: Structure of Proofs Up: No Title Previous: Algebra


This chapter contains an informal introduction to Nuprl \ proofs . It describes the structure of proofs, shows how to use the refinement  editor to move around in and add to proofs, and gives enough description and examples of rule usage to enable the reader to prove theorems of his own. Examples are drawn from logic (section 4.3) and elementary number theory (section 4.4). The reader may at times wish to refer to the complete presentation of the rules; this is contained in chapter 8.

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