Thursday 20 April 2017, 14:00, Room L106, Mines ParisTech, 60 bd St Michel, Paris: Habilitation, Olivier Hermant (Mines ParisTech).

Completeness in logics.

The work presented in my habilitation dissertation can be seen as completeness proofs of automatic theorem proving methods, in particular the tableaux method. Completeness is a result that allows to ensure that if an assertion is (universally) valid, an exhaustive search for a proof will succeed.

As we will see, these completeness results translate, first, into cut-free completeness results for sequent calculus, and then into cut admissibility theorems. In order to extend cut admissibility to more powerful logics, we then switch to more algebraic methods.

Lastly, we examine more thoroughly the cut admissibility proofs, and bring them closer to normalization proofs, in particular by studying how cut admissibilty, when it is proved constructively, generates cut-free proofs, yielding a cut elimination algorithm. We also study the semantic structures associated with normalization.

This work has been performed in various logical systems, for instance intensional higher-order logic (intuitionistic and linear), but the main domain of application is Deduction Modulo Theory, which adds to first-order deduction systems a rewrite relation on terms and formulas, and for which, in general, cut admissibility is undecidable. Nevertheless, most of the work presented in the dissertation has been handled generically.

Jury: