Proof Theoretic Applications of CERES

01.01.2010 - 30.04.2012
Forschungsförderungsprojekt
Proof-theoretic applications of CERES Alexander Leitsch Abstract Since the time of the ancient Greeks, proofs form the scientific backbone of mathematics. But proofs are not only verifications of theorems but also pieces of evidence and sources of new algorithms and mathematical methods. Proof analysis and proof transformations play a crucial role in this context; in particular the transformation of proofs into elementary ones (logically described as cut-elimination, which can - very roughly - be thought of as an application of Ockham's razor, as superfluous notions are removed from a proof) can be used to make hidden information explicit. With new theoretical methods and the increasing power of computers the computer- aided analysis of mathematical proofs becomes possible. Towards this aim, the method of cut-elimination by resolution (CERES) - in contrast to other methods of cut-elimination - has been applied successfully: the most prominent application was the analysis of Fürstenberg's proof of the infinity of primes, from which Euclid's (elementary) proof could be obtained. The CERES method, and the software system implementing it, have been developed, refined, and experimented with in the previous FWF projects P16264, P17995, and P19875. These past efforts, and the project we now propose, bring us closer to the long-range goal of making computer-aided proof analysis a standard tool for mathematicians. The first main issue tackled in this project is the further improvement of the CERES method: we know that cut-elimination by CERES is, in a certain sense, more powerful than the traditional, so-called reductive methods. Still, in practice the reductive methods may have the advantage that they are more deterministic than CERES. Our aim is therefore to describe the reductive methods as specific resolution refinements. Such refinements will be valuable, since the search of a resolution refutation has turned out to be the major bottleneck in the application of CERES to mathematical proofs, and the refinements will decrease this search space. Apart from increasing the efficiency of CERES, we intend to extend its scope: in its current formulation, CERES is not directly applicable to non-classical logics. We will develop and investigate modifications of CERES which can be used in these logics. The second main issue is the application of the refined CERES method to problems related to proof analysis. Among other aims, we will characterize classes of proofs where fast cut-elimination is possible by means of the resolution refinements, and we will extend the current results on CERES in higher-order logic to full higher-order logic, which will ease practical application of CERES as proofs can be formalized more naturally using higher-order logic.

Personen

Projektleiter_in

Projektmitarbeiter_innen

Institut

Grant funds

  • FWF - Österr. Wissenschaftsfonds (National) Austrian Science Fund (FWF)

Forschungsschwerpunkte

  • Computational Intelligence: 100%

Schlagwörter

DeutschEnglisch
Beweistheorieproof analysis
automatische Deduktionautomated deduction

Publikationen