A User-Level Introduction to the Nuprl Proof Development System

This document is intended to introduce the key elements of the Nuprl Proof Development System (Nuprl, for short) from the perspective of a Nuprl user, as opposed to the perspective of someone intimately involved in developing or extending Nuprl. As such, it may be more appropriate than other Kuprl-related documents for readers who are primarily concerned with uses of Nuprl and not fine details of Nuprl's mathematical foundation. It introduces and illustrates key Kuprl concepts -such as types, terms, displayforms, and tactics - in the framework of a model of calculational predicate logic inference.