Research on Automated Theorem Proving

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

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. ***