L'actualité partagée

Recherche

27/04/2017

Une HDR en logique

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.

Une HDR en logique - MINES ParisTech

L'actualité partagée - MINES ParisTech
Partager

contactez-nous

Des questions sur le musée ou la collection ? Contactez-nous

venir au musée

Retrouvez toutes les informations pour vous rendre au Musée de Minéralogie

Musée de Minéralogie

60 boulevard Saint Michel

75006 Paris

Ouvert :

Mardi - vendredi : 13h30 - 18h

Samedi : 10h - 12h30 et 14h - 17h

Fermé les dimanches, lundis et jours fériés

FERMETURE EXCEPTIONNELLE SAMEDI 30 JUIN

 

Contact Mentions légales efil.fr © 2014 MINES ParisTech