Thèse le Calcul Epsilon dans la Recherche de Preuves H/F

Institut Polytechnique de Paris École polytechnique

Le calcul epsilon de Hilbert est une formulation sans quantificateurs de la logique du premier ordre. En raison de sa syntaxe complexe, il n'a pas suscité beaucoup d'intérêt en vérification formelle. Cependant, le calcul epsilon peut offrir un gain de vitesse non élémentaire par rapport à des calculs plus classiques. Avec ce projet, je souhaite appliquer ce gain de vitesse au domaine de la démonstration de théorèmes automatisée et interactive.

The epsilon-calculus has been introduced by Hilbert in the beginning of the 20th century for his famous program on proving the consistency of mathematics. It provides an alternative syntax for predicate logic in which all quantifier information in a proof is encoded by epsilon-terms.

This quantifier-free formulation simplifies the reasoning about proofs, which led to some applications in the foundations of mathematics. However, due to its cumbersome syntax and unwieldy nature, the
epsilon-calculus has received little attention from the broader proof theory community, and it is not used at all in formal verification.

However, surprisingly, the epsilon calculus can provide a non-elementary speed-up over more standard formulations of first-order logic. This means that proofs carried out in the epsilon calculus can be shorter by a non-elementary factor than what we are used to from traditional proof systems,
like the cut-free sequent calculus. Given that first-order logic is undecidable in general, it would be highly desirable, if we could have proof search algorithms that have access to this speed-up, i.e., are able to find these shorter proofs. Even though there has been some investigation from the proof complexity viewpoint, there is no modern proof theoretical treatment of the epsilon calculus.

The purpose of this project is to make the advantages of epsilon calculus accessible to practitioners in formal methods, without having to suffer from the unreadable syntax mentioned above. For this, we plan to use the methods that have been developed within the last years around the area of
deep inference, which has proven to be successful in the area of propositional logics, admitting complexity benefits over traditional proof formalisms, such as exponential proof speed-ups
for certain tautologies and a quasipolynomial complexity cut-elimination procedure (in contrast to such procedures in the traditional sequent calculus, which have exponential complexity), as well as novel normalization procedures which are not exhibited by traditional proof formalisms, such
as new decomposition results and a confluent cut-elimination procedure.