Improving the Nuprl Proof Development System

Nuprl是一个支持形式化交互式开发的系统 数学 它被设计成特别适合 计算上重要的数学和建设 经过正式验证的软件。 Nuprl的实施，由 NSF于1984年完成。 从那时起，该系统已被用于 在康奈尔大学和其他地方进行了广泛的研究，作为进一步研究的基础。 这项研究在以下领域取得了重大进展： 自动推理和计算逻辑。 该系统已 成功地应用于广泛的问题，从验证 计算机硬件问题是程序设计理论中的一个公开问题 语言 它是许多文章和博士论文的主题。 本项目的目标是重写系统的一部分， 为了纳入某些扩展（反射机制）， 改进（新定义设施）。 这些都是基于几个 多年的研究和经验的系统。 他们将使 系统更容易访问，无论是在该地区的研究人员， 给其他人，比如数学家和教育家。 与 反射机制的实现，Nuprl将适用于 到目前难以治疗的领域。

Nuprl is a system supporting the interactive development of formal mathematics. It was designed to be especially suited to computationally significant mathematics and to the construction of formally verified software. The implementation of Nuprl, funded by the NSF, was completed in 1984. Since then the system has been used extensively at Cornell and elsewhere as a basis for further research. This research has resulted in significant advances in the areas of automated reasoning and computational logic. The system has been successfully applied to a wide range of problems, from verification of computer hardware to an open problem in the theory of programming languages. It has been the subject of many articles and PhD theses. The goal of the present project is to rewrite parts of the system in order to incorporate certain extensions (a reflection mechanism) and improvements (new definition facility). These are based on several years of study and experience with the system. They will make the system more accessible, both to researchers in the area and to others such as mathematicians and educators. With the implementation of the reflection mechanism, Nuprl will be applicable to domains that are currently difficult to treat.