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