U.S.-Germany Cooperative Research: Enhancing Proof Assistant Systems

该奖项支持Robert Constable和康奈尔大学的学生与德国萨尔大学计算机科学系的Joerg Siekmann的合作。由该奖项资助的研究将侧重于基于计算机的数学证明。目前的自动化定理证明了重要的定理，但必须搜索巨大的空间才能做到这一点，需要大量的时间和计算机资源，并且自动化工具和用户交互的组合是解决复杂问题所必需的。为了开发一种新的证明规划系统，本研究将改进计算机证明规划的知识获取，开发指导计算机定理证明搜索的技术，开发计算机数学库函数的标准，以及用户界面，这些结果将对工业和教育应用具有重要意义。这项联合合作的研究工作为初级研究人员提供了大量的机会，并且在这项提案上所做的工作将有助于使德国和美国研究小组之间的关系制度化。

0003789ConstableThis award supports Robert Constable and students from Cornell University in a collaboration with Joerg Siekmann of the Computer Science Department at the University of Saarland, Germany. The research funded by this award will focus on computer-based mathematical proofs. Current automated theorem prove non-trivial theorems, but must search huge spaces in order to do so, requiring a lot of time and computer resources, and a combination of automated tools and user interaction is necessary to solve complex problems. In order to develop a new breed of proof planning systems, this reseach will lead to improvements in knowledge acquisition for computer proof planning, development of techniques to guide searches in computer theorem proving, standards for computer mathematical library functions, and user interfaces Each of these results will have significance for industrial and educational applications. The opportunity this joint, collaborative research effort presents junior researchers is substantial, and the work done on this proposal will help institutionalize the relationship between the German and U.S. research groups.