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

美德合作研究：增强证明辅助系统

• 批准号: 0003789
• 负责人: Robert Constable
• 金额: $ 2.08万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-03-15 至 2004-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0003789&HistoricalAwards=false
• 关键词: U.S.; Germany; Cooperative; Research; Enhancing

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.

该奖项支持罗伯特·康斯特布尔和康奈尔大学的学生与德国萨尔兰大学计算机系的约尔格·西克曼合作。该奖项资助的研究将集中在基于计算机的数学证明上。目前的自动化定理证明非平凡定理，但需要搜索巨大的空间才能做到这一点，需要大量的时间和计算机资源，并且需要结合自动化工具和用户交互来解决复杂的问题。为了开发一种新型的证明计划系统，这项研究将促进计算机证明计划知识获取的改进，计算机定理证明中指导搜索的技术的发展，计算机数学库功能的标准和用户界面，这些结果都将对工业和教育应用具有重要意义。这种联合、合作的研究努力为初级研究人员带来了巨大的机会，就这一提议所做的工作将有助于使德国和美国研究小组之间的关系制度化。