BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//LORIA - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:LORIA
X-ORIGINAL-URL:https://www.loria.fr
X-WR-CALDESC:Évènements pour LORIA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20200329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20201025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20210328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20211031T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20220327T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20221030T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20210629T090000
DTEND;TZID=Europe/Paris:20210629T110000
DTSTAMP:20260406T170331
CREATED:20210622T094839Z
LAST-MODIFIED:20210622T094839Z
UID:12594-1624957200-1624964400@www.loria.fr
SUMMARY:Soutenance HDR : Sorin Stratulat (Mosel-Veridis)
DESCRIPTION: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. \nRésumé : \nLe 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. \nMots-clés : raisonnement par récurrence noethérienne\, raisonnement formel de premier ordre\, certification de preuves\, SPIKE\, Coq.\n  \nJury :\nRapporteurs :\nM. Adel Bouhoula\, Professeur\, Arabian Gulf University\, Bahreïn\nMme. Evelyne Contejean\, Directrice de recherche\, CNRS\nMme. Viorica Sofronie-Stokkermans\, Professeure\, Université de Coblence\, Allemagne \nExaminateurs :\nM. Tudor Jebelean\, Professeur\, Université Johannes Kepler\, Linz\, Autriche\nMme. Olga Kouchnarenko\, Professeure\, Université de Franche-Comté\nM. Stephan Merz\, Directeur de recherche\, INRIA\nM. Michaël Rusinowitch\, Directeur de recherche\, INRIA (parrain)\nMme. Jeanine Souquières\, Professeure\, Université de Lorraine \n 
URL:https://www.loria.fr/event/soutenance-hdr-sorin-stratulat/
LOCATION:C005\, Loria
CATEGORIES:HDR,Soutenance
END:VEVENT
END:VCALENDAR