This book includes a tutorial, a reference manual and a summary of research conducted on, and in, the system. The tutorial spans chapters 2 to 6. Chapter 2 presents a systematic foundational explanation of the mathematical theory underlying the Nuprl system, and it attempts to make the basic notions clear and self--evident. Chapter 3, with its collection of examples of statements in Nuprl , serves as the most concrete introduction to the system, and indeed certain readers may wish to start there. Chapter 4 introduces the reader to the Nuprl proof theory, again with lots of examples, and chapter 5 illustrates the system's function in the context of programming. Chapter 6 presents the metalanguage and the concept of tactics.
The reference section of this book comprises chapters 7 through 9. Chapter 7 details the organization of the system and contains a summary of commands and techniques users will find handy. Chapter 8 contains a brief account of the theoretical underpinnings of the system and gives a summary of the rules and ML constructors and destructors associated with the logic. Chapter 9 provides a detailed explanation of tactics.
The remaining chapters in this book consist of information and research results which will be of interest to the advanced user. Chapter 10 contains several recommendations about theory development which should prove extremely helpful for heavy users of Nuprl . Chapter 11 lays out a library of mathematical results we have obtained using the system, while chapter 12 presents recent developments in the logic which should be implemented by September 1985.
The remainder of this chapter discusses the place of in computer science research, specifically its relationship to logic, semantics, programming methodology, automated reasoning and intelligent systems. For those readers interested in research, this will provide both a motivation and a framework for further reading.