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

美法合作研究：自动定理证明器的理论与实现研究

• 批准号: 8715231
• 负责人: Jieh Hsiang
• 金额: $ 1.43万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1988
• 资助国家: 美国
• 起止时间: 1988-01-01 至 1991-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8715231&HistoricalAwards=false
• 关键词: U.S.; France; Cooperative; Research; Studies

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.

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