Proof Transformations via Cut-Elimination in Intuitionistic Logic

Proofs are the scientific backbone of mathematics since the time of the Greeks. They are not just verifications of theorems, but also pieces of evidence and sources of algorithms and mathematical methods. In the culture of mathematical proofs proof transformations play a crucial role; in particular the transformation of proofs into elementary ones (logically described by cut-elimination) allows the extraction of bounds and algorithms and, finally, also of programs. A program for automated cut-elimination of proofs (expressed in the Gentzen calculus LK) has been developed in several FWF-projects on the basis of the method CERES (cut-elimination by resolution). This program has been applied successfully to the analysis of interesting mathematical proofs. Its efficiency is based on the use of automated theorem proving which forms the real core of the method. CERES has been defined for classical logic (first- and higher-order) and some classes of many-valued logics. The purpose of this project is the extension of CERES to intuitionistic logic (concerning proof analysis in mathematics, intuitionistic logic is, apart from classical logic, the most important one). In fact, using the classical CERES-method of cut-elimination on intuitionistic proofs with cuts (in contrast to Gentzen`s method) mostly results in classical cut-free proofs, making an adjustment of the method necessary. The aim is to develop two basic CERES-type methods for intuitionistic logic; one of them (the more conservative one) should use a resolution calculus for intuitionistic logic and change the current classical CERES-method in a minimal way; the other should explore the use of different calculi (e.g. of LJ itself) for the proof search phase of the method. Moreover we plan a thorough investigation, when and how classical cut-free proofs, obtained by application of classical CERES on intuitionistic proofs, can be transformed into intuitionistic ones. The developed methods will be implemented and tested on a mathematical proof in the area of linear algebra. Intuitionistic logic possesses a natural computational interpretation via the Curry-Howard isomorphism (between natural deduction and typed lambda-calculus). We plan to investigate the impact of intuitionistic CERES to the execution of functional programs (via the corresponding proof normalization); in fact, executing a program via CERES might be much more efficient than applying beta- reduction. The theoretic and practical work on the method should eventually result in a system of automated and semi- automated proof transformation for intuitionistic logic (as it already exists for classical one) accessible to mathematicians; to them it should provide a support for the analysis and development of mathematical proofs.

Cut-elimination is a technique of proof transformation serving the purpose of extracting relevant information from proofs (this information may consist of a witness for an existential statement or of a computable function). Cut-elimination makes implicit information explicit and is thus a main technique for mining proofs. As this proof transformation is very technical and involved it is usually not possible to do it by hand unless for quite simple proofs. The standard method of cut-elimination (derived from a famous proof by Gerhard Gentzen in 1935) is based on stepwise reduction of proofs and is very redundant and inefficient. The method CERES (cut-elimination by resolution) is a newer method (developed around 2000) which analyzes the whole proof in a preprocessing step and reduces cut-elimination to a theorem proving problem (which then can be solved by methods of automated deduction). CERES was defined first for first-order logic and then for higher-order logic. The problem of extending the method to intuitionistic logic (a logic which is more constructive and informative than classical logic, though harder to handle) was largely solved in the project. As intuitionistic logic (like classical logic) is a main tool for modeling mathematical proofs, the development of efficient methods for proof analysis is of major importance. In this project the method CERES was adapted to intuitionistic logic and compared to the traditional cut-elimination method l Gentzen. Like in CERES for classical logic the efficiency of the method could be substantially increased. However the method is less uniform and behaves quite differently on different classes of proofs. Besides a development of a method for intuitionistic logic, the analysis carried out in the project led also to an improvement of the original method for classical logic. The project contributes to the better understanding of mathematical proofs by the development of more efficient and automatable methods for proof analysis.