Accueil

webTV

Lecture

Conférence éthique et intelligence artificielle : Elise Berlinski

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Carlos Adrian Correa Florez, MINES ParisTech PhD, PERSEE center

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Lancement de la Chaire industrielle ANR TOPAZE

+ TOUS

contact

Retrouvez nos coordonnées
sur la page
Informations pratiques

Actualité de la délégation de Fontainebleau

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

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

Actualité de la délégation de Fontainebleau - MINES ParisTech
Partager

actualité

Le Rapport d'activité 2020 est en ligne

Formation Le Rapport d'activité 2020 est en ligne MINES ParisTech, établissement-composante…
> En savoir +

Une santé de fer !<br>
Minéraux et santé, de l'Antiquité à nos jours

Formation Une santé de fer ! Minéraux et santé, de l'Antiquité à… Sous la plume de Quentin Bollaert, Alexandre Couturier,…
> En savoir +

Pourquoi éclipser le solaire ?

Formation Pourquoi éclipser le solaire ? Le rapport « Electricité : le devoir…
> En savoir +

DigiTraining lance un appel aux musées européens

International DigiTraining lance un appel aux musées européens Innover grâce aux nouvelles technologies Le…
> En savoir +

EcorcAir et les platanes du Quartier latin

Formation EcorcAir et les platanes du Quartier latin Vendredi 2 avril 2021, dernier jour de cours, en…
> En savoir +

Rentrée 2021 du MS MSIT (Mines - Dauphine)

Formation Rentrée 2021 du MS MSIT (Mines - Dauphine) La nouvelle promotion MS MSIT aura sa rentrée…
> En savoir +

+ Toutes les actualités

agenda

Du 20 juillet 2021 au 3 janvier 2022 Rentrée 2021 - 2022

Du 20 juillet 2021 au 3 janvier 2022 Rentrée 2021 - 2022

+ Tous les événements

Plan du site
Contacts Mentions légales efil.fr © 2014 MINES ParisTech