Contents

• Contents
• Introduction
  • Brief Overview
  • Previous Work
  • Proposed Work
• Sample of Formal Reference Mathematics and Lesson
  • Research Technology in Education
  • Example of Reference Material
  • Hypertext, Terms, and Proofs
  • Sample Lesson
• The Nuprl Computational Mathematics Medium
  • The Formal Language
  • Tactic-style Theorem Provers
  • Fragment of Algebra Library
  • Built-in Functional Programming Language
  • Library Structure and Use
• Educational Aspects
  • Problems and Opportunities
  • Experience with Students Learning Discrete Mathematics and Logic
  • Evaluation and Monitoring
  • Exploration and Collaboration
  • Criticisms
• Work Plan
  • Background
  • Schedule and Milestones
• An Exercise in Induction
• Summary and Impact
• References
• About this document ...

Results From Prior NSF Support
The project started with NSF grant DUE-955162, duration January 1996-December 1997. Narrative about previous results appears in section 1.2 Previous Work of the proposal. Basically, we have created a large body of formal courseware and some targeted lessons built on it. We designed and implemented software to present this material on the Web to be viewed with Netscape and Explorer. The material was used in Cornell courses and is now available to be used elsewhere. There were two publications [24][21] in the eighteen months since we have been funded plus three "Web publications."

The course material can be accessed at the following url:
www.cornell.edu/Info/Projects/NuPrl/html/Interactive_Formal_Courseware.html.