Bienvenue aux Mines Paristech
Bienvenue à MINES ParisTech
Newsletter International
Website
Théorie & Pratique
Vous êtes

rechercher
une actualité

Ecole
Entreprise
Formation
International
Recherche
Sciences de la terre et
de l'environnement
Energétique et procédés
Mécanique et matériaux
Mathématiques et systèmes
Economie, management
et société
Partager

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

webTV

Lecture

Entretien avec Pierre LAFFITTE

Lecture

Uranium : modéliser le transport réactif

Lecture

Comment devenir ingénieur par la formation continue

Lecture

Histoires de sciences et entreprises

Lecture

Qu'est ce que I'internet Physique ?

+ Toutes les vidéos

actus / Sciences de la terre et l'environnement

Consulter les actus de cette thématique

actus / Énergétique et procédés

Consulter les actus de cette thématique

actus / Mécanique et matériaux

Consulter les actus de cette thématique

actus / Mathématique et systèmes

Consulter les actus de cette thématique

actus / Économie, management et société

Consulter les actus de cette thématique
Plan du site
MINES
ParisTech

60, Boulevard Saint-Michel
75272 PARIS Cedex 06
Tél. : +33 1 40 51 90 00

Implantations
Formation
Mentions légales | efil.fr | ©2012 MINES ParisTech | +33 1 40 51 90 00 |