The Book

Implementing Mathematics with The Nuprl Proof Development System

Next: Contents   Contents

• Contents
• Overview
  • Brief Description of Nuprl
  • Highlights of Nuprl
  • Motivations
  • The Nuprl Logical Language
  • Components of the Nuprl System
    • General
    • Definitions
    • Proof Editing
    • Evaluation
  • Programming Modes
  • Physical Characteristics
  • The ``Feel'' of the System
  • This Document
    • Scope
    • Organization
  • Research Topics
    • Programming Languages
    • Semantics
    • Methodology and Verification
    • Environments
    • Theorem Proving
    • Program Synthesis
    • Artificial Intelligence
  • Related Work
    • Close Relatives
    • Intuitionism and Type Theory
    • Theoretical Background
    • Systems Background
  
  
• Introduction to Type Theory
  • The Typed Lambda Calculus
    • A Formal System
    • Computation System
  • Extending the Typed Lambda Calculus
    • Dependent Function Space
    • Cartesian Product
    • Dependent Products
    • Disjoint Union
    • Integers
    • Atoms and Lists
  • Equality and Propositions as Types
    • Propositions as Types
  • Sets and Quotients
  • Semantics
  • Relationship to Set Theory
  • Relationship to Programming Languages
  
  
• Statements and Definitions in Nuprl
  • Overview of the Nuprl Environment
    • Windows
    • Commands and Status
    • Starting Up
    • Finishing Up
  • Libraries
    • Entry of Objects
    • Saving Results
  • The Text Editor
    • Entering Text
    • Copying Text
  • Definitions
  • Syntactic Issues
    • Theorems
    • Expressions Formed by Using Type Constructors
  • Stating Theorems
    • Expressing Concepts in the Language of Types
    • Propositions as Types
  • Defining Logics
    • Constructive Logic
    • Classical Logic
    • Other Logical Operators
  • Elementary Number Theory
  • Set Theory
    • The Subset Constructor
    • Intervals
  • Algebra
  
  
• Proofs
  • Structure of Proofs
  • Commands Needed for Proofs
  • Examples from Introductory Logic
    • Constructive Propositional Logic
    • Classical Propositional Logic
    • Predicate Logic
  • Example from Elementary Number Theory
  
  
• Computation
  • Term Extraction
  • Evaluation
    • Using the Evaluator
    • The Reduction Rules
    • The Reduction Strategy
    • Properties of the Evaluator
  • Computational Content
  • An Example
  
  
• Proof Tactics
  • Refinement Tactics
  • Transformation Tactics
  • Writing Simple Tactics
    • The Metalanguage ML
    • Using ML from Nuprl
    • Example Tactics
    • The Auto-tactic
  
  
• System Description
  • The Command Language
    • Library Display
    • Manipulating Objects
    • Storing Results
    • General Commands
  • The Library
    • Object Types
    • Library Entries
  • Window Management
    • Mouse Mode
    • Positioning the Mouse Cursor
    • Adjusting and Moving Windows
    • Other Keys in Mouse Mode
  • The Text Editor
    • Tree Cursors, Tree Positions and Bracket Mode
    • Moving the Cursor
    • Adding Text
    • Deleting and Killing Text
    • Copying and Moving Text
  • The Proof Editor
    • Basics of the Proof Editor
    • Motion within a Proof Node
    • Motion within the Proof Tree
    • Initiating a Refinement
    • Showing Goals, Subgoals and Rules
    • Invoking Transformation Tactics
  • Definitions and Definition Objects
  
  
• The Rules
  • Semantics
    • Substitution
    • The Computation System
    • The Type System
    • Judgements
  • The Type System in Detail
    • Formal Definition of Equality
    • Typehood and Membership
  • The Rules
    • The Form of a Rule
    • Organization of the Rules
    • Specifying a Rule
    • Optional Parameters and Defaults
    • Hidden Assumptions
    • Shortcuts in the Presentation
  • ATOM
  • VOID
  • INT
  • LESS
  • LIST
  • UNION
  • FUNCTION
  • PRODUCT
  • QUOTIENT
  • SET
  • EQUALITY
  • UNIVERSE
  • MISCELLANEOUS
  • ML Constructors
  • ATOM
  • VOID
  • INT
  • LESS
  • LIST
  • UNION
  • FUNCTION
  • PRODUCT
  • QUOTIENT
  • SET
  • EQUALITY
  • UNIVERSE
  • MISCELLANEOUS
  
  
• The Metalanguage
  • An Overview of ML
    • Functional Style
    • Type Definitions
    • Polymorphic Typing
    • Failures
    • Syntax and Semantics
    • Using ML in Nuprl
  • Tactics in ML
  • Basic Types in ML for Nuprl
    • Proofs
    • Rules
    • Declarations
    • Terms
    • Print Representation
    • A Note about Equality
  • Tools for Tactic Writers
    • Tacticals
    • Substitution
    • Unification
  • Example Tactics
    • Example Transformation Tactics
    • A Larger Example
  • Existing Tactics
  
  
• Building Theories
  • Proofs
  • Definitions
  • Sets and Quotients
  • Theories
  
  
• Mathematics Libraries
  • Basic Definitions
  • Lists and Arrays
  • Cardinality
  • Regular Sets
  • Real Analysis
  • Denotational Semantics
  
  
• Recursive Definition
  • Inductive Types
    • Expressiveness and Elegance
  • Details of the Extension
    • Computation System Modification
    • Inductive Type Proof Rules
      • Formation
      • Intro
      • Elim
      • Computation
  • Example Proof
  • Partial Function Types
  • Details of the Extension
    • Computation System Modification
    • Domain Predicate
    • Partial Function Type Proof Rules
      • Formation
      • Intro
      • Elim
      • Computation
  • General Notes
  • Refinement Functions
  • Rule Constructors
  • Rule Destructors
  • Term Destructors
  • Auto-Tactic
  • Miscellaneous Functions
  • Differences in the Logic
    • Introduction Rules
    • Elimination Rules
    • Equality and Simplification Rules
  • Differences in the User Interfaces
  • Simulating Lambda-prl Constructs in Nuprl
    • Logical Operators
    • Lists
    • Primitive Recursive Functions
    • Extraction Terms
  
  
• Bibliography
• About this document ...

Important note about this book

The Nuprl math library is constantly evolving, expanding, and refining. This text, written in 1985, provides useful descriptions and background information for using Nuprl. However many of the mathemacial projections have been updated and no longer exist in the library . Please see the Math Library and Publications list for more recent projections.

Implementing Mathematics with The Nuprl Proof Development System

By the PRL Group:
R. L. Constable
S. F. Allen
H. M. Bromley
W. R. Cleaveland
J. F Cremer
R. W. Harper
D. J. Howe
T. B. Knoblock
N. P. Mendler
P. Panangaden
J. T Sasaki
S. F. Smith

Available from Amazon and other retailers.

This research supported in part by the National Science Foundation under grant DCR83-03327.
Copyright © 1985 by R. L. Constable and Prentice-Hall.