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

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

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.