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

点击翻译按钮获取中文摘要

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.