A User-Level Introduction to the Nuprl Proof Development System
Eric Aaron · ScholarlyCommons (University of Pennsylvania) · 2001
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.