Automated Analysis of Mathematical Proofs

Proofs are the scientific backbone of mathematics since the time of the Greeks. They are not only verifications, but also pieces of evidence and sources of algorithms and mathematical methods. In this context PROOF ANALYSIS and proof transformations play a crucial role; in particular the transformation of proofs into elementary ones (logically described by cut-elimination) allows for the extraction of Herbrand sequents, of bounds and of algorithms (finally also of programs). A program for automated cut-elimination (expressed in the Gentzen calculus LK) has been developed in the FWF-project P 16264 on the basis of the method CERES (cut-elimination by resolution). This program proved capable of eliminating cuts in large and complex LK-proofs; its efficiency is based on the use of the resolution method which forms the real core of the method. The purpose of this project is a twofold one: (1) to extend the range of the CERES method to real mathematical proofs. To this aim we plan to develop specific intermediary proof languages (based on introduction and elimination of definitions) and a proof editor allowing for the comfortable input of large and complex proofs. In the kernel of the algorithmic method we plan to extend CERES to equality and to define efficient algorithms for the extraction of Herbrand sequents. (2) We intend to deepen the theoretical analysis of CERES in particular concerning higher-order logic and intuitionistic logic. This could lay the ground for efficient proof transformations in higher-order mathematics. The theoretic and practical work on the method should eventually result in a system of automated and semi-automated proof transformation accessible to mathematicians; to them it should provide a support for the analysis and development of mathematical proofs.

Proofs are the scientific backbone of mathematics since the time of the Greeks. They are not only verifications, but also pieces of evidence and sources of algorithms and mathematical methods. In this context PROOF ANALYSIS and proof transformations play a crucial role; in particular the transformation of proofs into elementary ones (logically described by cut-elimination) allows for the extraction of Herbrand sequents, of bounds and of algorithms (finally also of programs). A program for automated cut-elimination (expressed in the Gentzen calculus LK) has been developed in the FWF-project P 16264 on the basis of the method CERES (cut-elimination by resolution). This program proved capable of eliminating cuts in large and complex LK-proofs; its efficiency is based on the use of the resolution method which forms the real core of the method. The purpose of this project is a twofold one: (1) to extend the range of the CERES method to real mathematical proofs. To this aim we plan to develop specific intermediary proof languages (based on introduction and elimination of definitions) and a proof editor allowing for the comfortable input of large and complex proofs. In the kernel of the algorithmic method we plan to extend CERES to equality and to define efficient algorithms for the extraction of Herbrand sequents. (2) We intend to deepen the theoretical analysis of CERES in particular concerning higher-order logic and intuitionistic logic. This could lay the ground for efficient proof transformations in higher-order mathematics. The theoretic and practical work on the method should eventually result in a system of automated and semi-automated proof transformation accessible to mathematicians; to them it should provide a support for the analysis and development of mathematical proofs.