Improving the Nuprl Proof Development System

Nuprl是一个支持形式数学交互式开发的系统。它被设计为特别适合于计算意义重大的数学和构造正式验证的软件。由美国国家科学基金会资助的Nuprl的实施于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.