Research on Automated Theorem Proving

自动定理证明研究

• 批准号: 9307731
• 负责人: Woodrow Bledsoe
• 金额: $ 11.84万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1994
• 资助国家: 美国
• 起止时间: 1994-03-15 至 1997-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9307731&HistoricalAwards=false
• 关键词: Research; Automated; Theorem; Proving

9307731 Bledsoe This renewal project continues the effort to build more powerful theorem provers with automated proof discovery as the central focus. The principal problem domain is mathematics with offers a rich source of theorems that automated provers cannot yet prove. Methods developed for mathematics apply to many areas, such as reasoning in expert systems, inference in large databases, program verification, reverse engineering, factory automation, etc. The work focuses on basic heuristic methods either modelled from human behavior or discovered through analysis of individually targeted domains. Specifically, the research focuses on "large- step" methods, second order logic, analogy, proof plans or scripts, interactive theorem proving, and the combining of these efforts Implementation of analogy in automatic proof discovery remains an important long term goal. Analogy as used by mathematicians is an extremely powerful proof methodology. This project uses proof plans and scripts, and centers on proving a few very difficult theorems with analogy. ***

9307731布莱索这个更新项目继续努力构建更强大的定理证明器，以自动证明发现为中心焦点。 主要的问题领域是数学，它提供了丰富的自动证明器还不能证明的定理。 为数学开发的方法适用于许多领域，如专家系统中的推理，大型数据库中的推理，程序验证，逆向工程，工厂自动化等。 这项工作的重点是基本的启发式方法，无论是从人类行为建模或通过分析个别目标域发现。 具体地说，研究集中在“大步”方法、二阶逻辑、类比、证明计划或脚本、交互式定理证明以及这些努力的结合。 在自动证据发现中实现类比仍然是一个重要的长期目标。 数学家使用的类比是一种非常强大的证明方法。 这个项目使用证明计划和脚本，并集中在证明一些非常困难的定理与类比。 ***