U.S.-France Cooperative Research: Studies in the Theory and Implementation of Automated Theorem Provers

该奖项将支持纽约州立大学石溪分校的Jieh Hsiang教授和巴黎第南大学奥赛中心的Jean-Pierre Jouannaud教授在自动定理证明领域的合作研究。这项工作的目的是以一种有效的方式调查这些研究者开发的大量定理证明策略的有用性。在基于反驳策略的推导中，研究人员最关注的是包含相等和删除推理规则的策略，这两种策略在推导中得到了最有效的利用。他们将发展一个表达反驳策略的框架。利用这个框架以及一种新的证明技术，这种证明技术已经成功地证明了各种定理证明方法的完备性，他们将开始开发一个统一的编程环境，用于生成和实验计算机化的定理证明。法国合作者在人工智能和自动定理证明领域有相当丰富的经验。与美国研究人员的合作研究始于1983年，涉及两个实验室的人员交流，并在目前工作要扩展的领域取得了相当大的进展。研究结果可能对定理证明器和证明检查器的未来设计和实现以及人工智能本身的理论基础产生重大影响。

This award will support collaborative research between Prof. Jieh Hsiang of the State University of New York at Stony Brook, and Prof. Jean-Pierre Jouannaud, University of Paris-Sud, Centre d'Orsay, in the area of automated theorem proving. The objective of this work is to investigate in an efficient manner the usefulness of a large number of theorem-proving strategies developed by these investigators. The researchers are most involved with strategies involving equality and deletion inference rules, which are utilized most efficiently in derivations based upon refutational strategies. They will develop a framework for expressing refutational strategies. Using this framework as well as a new proof technique which has been successful in proving the completeness of a wide variety of theorem proving methods, they will begin development of a uniform programming environment for producing and experimenting with computerized theorem provers. The French collaborator has considerable experience in the field of artificial intelligence and automated theorem proving. Cooperative research with the U.S. investigator dates to 1983, involving exchanges of individuals from both laboratories and has resulted in considerable progress in the areas to be extended by the current work. The research results could have a significant impact on the future design and implementation of theorem provers and proof checkers, and on the theoretical basis of artificial intelligence itself.