U.S.-Germany Cooperative Research: Enhancing Proof Assistant Systems

Cornell University, Ithaca NY

Investigators

Abstract

0003789 Constable This award supports Robert Constable and students from Cornell University in a collaboration with Joerg Siekmann of the Computer Science Department at the University of Saarland, Germany. The research funded by this award will focus on computer-based mathematical proofs. Current automated theorem prove non-trivial theorems, but must search huge spaces in order to do so, requiring a lot of time and computer resources, and a combination of automated tools and user interaction is necessary to solve complex problems. In order to develop a new breed of proof planning systems, this reseach will lead to improvements in knowledge acquisition for computer proof planning, development of techniques to guide searches in computer theorem proving, standards for computer mathematical library functions, and user interfaces Each of these results will have significance for industrial and educational applications. The opportunity this joint, collaborative research effort presents junior researchers is substantial, and the work done on this proposal will help institutionalize the relationship between the German and U.S. research groups.