JavaScript is disabled for your browser. Some features of this site may not work without it.
Formalizing Constructive Real Analysis

Author
Forester, Max B.
Abstract
This paper arises from a project with the Nuprl Proof Development System which involved formalizing parts of real analysis, up through the intermediate value theorem. Extensive development of the rational library was required as the real library was being built, resulting in the addition of about 125 rational theorems. The real library now contains about 150 theorems and includes enough basic results that further extensions of the library should be quite feasible. This paper aims to illustrate how higher mathematics can be implemented in a system like Nuprl, and also to introduce system users to the library.
Date Issued
1993-09Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR93-1382
Type
technical report