Accueil

• Agenda
• Actualité

Actualité de la délégation de Fontainebleau

Retrouvez toutes les actualités et faits marquants ...

Une HDR en logique

Olivier Hernant, chercheur à MINES ParisTech, soutient son HDR.

Olivier Hermant, du Centre de recherche en informatique de MINES ParisTech, a soutenu son Habilitation à diriger des recherches de l'Université Paris Diderot, le jeudi 20 avril, à MINES ParisTech. Le sujet de ses travaux est la "Complétude en logiques". 

Le jury, international, constitué des rapporteurs Delia Kesner, Dale Miller et Sara Negri, accompagnés des examinateurs Gilles Dowek, Catherine Dubois, Alessio Guglielmi, Pierre Jouvelot et Alexander Leitsch, ont unanimement loué la qualité des travaux d'Olivier au cours des années précédentes ; on en trouvera ci-dessous la description (en anglais).

"Complétude en logiques". 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 an elimination algorithm. We also study the semantic structures associated with proof 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.