U.S.-Germany Cooperative Research to Enhance the Performance of the Model Elimination Proof Procedure

美德合作研究提高模型消除证明程序的性能

• 批准号: 9514375
• 负责人: Donald Loveland
• 金额: $ 1.31万
• 依托单位: Duke University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-07-15 至 1999-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9514375&HistoricalAwards=false
• 关键词: U.S.; Germany; Cooperative; Research; Enhance

This award supports Professor Donald Loveland and Assistant Professor Owen Astrachan of Duke University to collaborate in computer science research with Professor Eike Jessen and others of the Computer Architecture Department of the Technical University of Munich (TUM), Germany. They are studying the Model Elimination proof procedure, a general-purpose theorem-proving technique of interest to both research groups. The procedure is derived from the logic programming language Prolog, and can use the sophisticated implementation architecture developed for Prolog. There is a significant amoung of research being performed on Model Elimination in Germany as part of a five year multi-university research program on deduction that is lead by the TUM group. A fundamental issue being studied by both the German and US groups is the intelligent use of lemmas that are automatically generated by the Model Elimination system for use in accelerating the subsequent proof finding. Significant theorems have been proven using this technique enhanced with the lemma device where no solutions would have been possible without the lemma device. Therefore the development of good lemma selection techniques would be particularly valuable in this area of computer science. The collaborating Duke and TUM research groups have experience respectively with global and local lemma techniques. These are quite different approaches, and combining them is expected to lead to enhancements of the lemma techniques which will expand the usefulness of the Model Elimination procedure for proving more complex theorems such as those in the `grand challenge` class. The U.S. group will also benefit from interactions with other participants in the German national program from the University of Koblenz and the Humboldt University in Berlin.

该奖项支持杜克大学的Donald洛夫兰教授和Owen Astrachan助理教授与德国慕尼黑工业大学（TUM）计算机体系结构系的艾凯Ewen教授和其他人在计算机科学研究方面进行合作。 他们正在研究模型消除证明过程，这是两个研究小组都感兴趣的通用定理证明技术。 该程序是从逻辑编程语言Prolog派生的，可以使用为Prolog开发的复杂的实现架构。 在德国，作为由TUM集团领导的一个为期五年的多大学演绎研究计划的一部分，正在进行大量关于模型消除的研究。 德国和美国研究小组正在研究的一个基本问题是智能地使用由模型消除系统自动生成的引理，用于加速随后的证明发现。 重要的定理已被证明使用这种技术增强了引理设备，没有解决方案将是不可能的引理设备。 因此，良好的引理选择技术的发展将是特别有价值的，在这方面的计算机科学。 合作的杜克和TUM研究小组分别与全球和本地引理技术的经验。 这些是完全不同的方法，并将它们结合起来，预计将导致增强的引理技术，这将扩大有用的模型消除程序证明更复杂的定理，如那些在“大挑战”类。 美国小组还将受益于与来自科布伦茨大学和柏林洪堡大学的德国国家项目的其他参与者的互动。