Sorin Stratulat, Maître de conférences dans l’équipe Mosel-Veridis, soutiendra son HDR : intitulée : “Noetherian Induction for Computer-Assisted First-Order Reasoning/Récurrence noethérienne pour le raisonnement de premier ordre et assisté par l’ordinateur”. Celle-ci se déroulera en anglais le mardi 29 juin à partir de 9h00 en salle C005 du Loria. Le nombre de places étant limité, elle sera aussi accessible en distanciel.
Résumé :
Le principe de la récurrence noethérienne est un des plus généraux principes du raisonnement formel. Dans le cadre du raisonnement de premier ordre, nous proposons une classification de ses instances pouvant être partagées en instances basées sur des termes et sur des formules. Nous donnons un aperçu du raisonnement par récurrence noethérienne basé sur des termes et des formules, et établissons des relations entre eux. Nous montrons que toute preuve intégrant du raisonnement par récurrence noethérienne basée sur des termes peut être convertie en une preuve dont le raisonnement par récurrence est basé sur des formules. La question de la conversion dans l’autre direction reste ouverte. Pourtant, nous identifions certaines classes de preuves par récurrence noethérienne basée sur des formules qui peuvent être traduites en des preuves dont le raisonnement par récurrence est basé sur des termes. Nous établissons des liens entre le raisonnement noéthérien basé sur des formules et d’autres types de raisonnement formel de premier ordre, comme le raisonnement par récurrence cyclique pour la logique de premier ordre avec des définitions inductives (FOLID) et le raisonnement basé sur la saturation. Nous avons mis au point des méthodologies pour certifier le raisonnement noethérien basé sur des formules et le raisonnement cyclique pour FOLID en utilisant l’assistant de preuve Coq.
Jury :
Rapporteurs :
M. Adel Bouhoula, Professeur, Arabian Gulf University, Bahreïn
Mme. Evelyne Contejean, Directrice de recherche, CNRS
Mme. Viorica Sofronie-Stokkermans, Professeure, Université de Coblence, Allemagne
Examinateurs :
M. Tudor Jebelean, Professeur, Université Johannes Kepler, Linz, Autriche
Mme. Olga Kouchnarenko, Professeure, Université de Franche-Comté
M. Stephan Merz, Directeur de recherche, INRIA
M. Michaël Rusinowitch, Directeur de recherche, INRIA (parrain)
Mme. Jeanine Souquières, Professeure, Université de Lorraine
