About Schemata and Proofs

The aim of this project is to develop theoretical frameworks for handling formula schemata and proof schemata in interactive (or automated) theorem proving, and use these schemata calculi to help in the formalisation and analysis of mathematical proofs (via proof-theoretical transformation techniques by cut-elimination). The considered schemata are iteration schemata which are ubiquitous in mathematics and in computer science. Typical examples include the pigeonhole principle and Ramsey`s theorem. These schemata also occur frequently for instance in circuit or program verification where the modelling formulae are frequently parameterized by a natural number (denoting for instance the number of bits, the size of the data, etc.). Reasoning with such formulae is difficult and usually requires some form of mathematical induction. Designing proof procedures able to do that automatically would significantly increase the expressive power and allow the construction of shorter, more informative and structured proofs. The use of iterated schemata is extremely useful for the formalization of mathematical proofs, which is the subject of the present proposal, because it allows one to express infinite proof sequences in a very natural and convenient way. This idea has been used in the system HLK/CERES (developed by Partner 2) for the analysis of mathematical proofs in order to formalise inductive proofs without having to work with too expressive logical formalisms (for which no efficient proof procedures exist). However, the current system only allows to define such iteration sequences and the obtained schemata have to be reduced to first-order proofs by instantiation before being processed. In the present project, we intend to design tools for handling these sequences directly at the object level and for reasoning with them (in an automated and/or interactive way). We want to define appropriate "intermediate" logical formalisms, whose expressive power should be greater than the base language (e.g. first-order logic) but lower than full higher-order languages. The obtained language should be more expressive in some respect than the original one and allow more natural and concise formalisations, but it should also preserve - when possible - some of the good computational properties of the original language, e.g. decidability or completeness. The project, being centered around formula/proof schematisation and their applications in computer mathematics, is directly related to the thematic axe "Mathematics", as well as to logic, proof theory and, of course, automated deduction. To the best of our knowledge, there are no other projects with similar aims.

The main working tool of a mathematician is proof: through proof, truth is established, and reasons are explained. The development of mathematical logic in the 19th and 20th century has uncovered the notion of formal proof: a mathematical proof is viewed as a discrete object which can be manipulated algorithmically, that is: by a computer. This has lead to the study of computational logic, which is concerned with the study of logical formalisms with respect to mechanization or automatization. An important notion that is studied in computational logic is that of cut-elimination: an algorithm that, from a formal proof, computes another formal proof of the same theorem that is direct, it does not include any detours. Such proofs are important since useful information can be extracted from them completely automatically: e.g. explict algorithms and upper bounds. It is an important aspect of computational logic to apply abstract techniques such as cut-elimination to concrete formalized proofs in order to reveal new information hidden in the indirect parts of the proof.The interplay of cut-elimination with the most important mathematical method of proof, complete induction, which lies at the core of our understanding of the natural numbers, is at the heart of the research that was performed in this project. It was already well-known that cut-elimination in the presence of induction is in general impossible, and the aim of this project was to extend the reach of cut-elimination into the realm of inductive proofs by combining a novel approach to cut-elimination with a novel approach to inductive proofs: the CERES (cut-elimination by resolution) method, a method of cut-elimination based on resolution theorem proving which has many good properties, was combined with the notion of proof schemata, which characterize a certain class of inductive proofs in a natural way.In the course of the project, the existing notion of propositional formula schemata was generalized to first-order proof schemata, a necessary step to strengthen the formalism to be able to cope with real-world mathematical proofs. The notion of first-order proof schemata, and its link to inductive proofs, was thoroughly investigated. The technical machinery of the CERES method was generalized to the setting of schemata, and based on this machinery, the CERESS (schematic CERES) method was developed and theoretically investigated, leading to a notion of schematic ACNF (atomic cut normal form), which describes an infinite sequence of cut-free proofs in a schematic manner. On the one hand, this result opens the way for practical applications of CERESS to extract information from real-world inductive proofs and on the other hand, it raises several interesting theoretical questions regarding the nature of schematic proofs and cut-elimination.