Educational Innovation: Creating and Evaluating Formal Courseware for Mathematics and Computing

这个CISE教育创新奖支持开发用于数学和计算教学的交互式正式基础课件。 该课件由现代证明开发系统Nuprl创建，基于其正式计算数学参考库。 该项目建立在该领域早期工作的基础上，1）将有针对性的课程作为正式数学语料库的入口点，2）收集学生和教师的反馈以进行评估，3）包括1999年在Web上可用时利用完整的Nuprl交互功能所需的工作。 该项目通过修改现有的研究工具，并结合机器辅助推理实践的想法，创造易于使用和新颖的教育技术，以使数学文本的传统逻辑结构变得清晰。 它有可能产生广泛的影响。

This CISE Educational Innovation award supports the development of interactive formally-grounded courseware for teaching both mathematics and computing. The courseware is created by a modern proof development system, Nuprl, based on its reference library of formal computational mathematics. This project builds on earlier work in the area and 1) adds targeted lessons as entry points to the corpus of formal mathematics, 2) gathers feedback from students and instructors for evaluation purposes, and 3) includes work necessary for utilizing the full Nuprl interactive capability when it becomes available on the Web in 1999. The project is creating easily used and novel educational technology by modifying existing research tools and incorporating ideas from the practice of machine assisted reasoning to make plain the conventional logical structure of mathematics text. It has the potential to make a broad impact.