About Schemata And Proofs – ASAP

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 handle schemata in an automatic way would significantly increase the expressive power and allow for shorter, more enlightening and structured proofs. The use of iterated schemata is extremely useful for the formalization of mathematical proofs 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 proof in order to formalise inductive proofs without having to work with too expressive logical formalisms (for which no adequate 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). More precisely, 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 qualitative improvements added by the results of this project to automated theorem provers and proof assistants have been since the very beginning identified as very desirable by the users of these systems, in particular by the mathematicians. The project, devoted to 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. As far as we know, there are no other projects with similar aims.