MARDI 23 NOVEMBRE 2021 APRES-MIDI

MERCREDI 24 NOVEMBRE MATIN

JOURNEE(S) LOGIQUE ET INTERACTION

dans le cadre des actions transverses du LIRMM

=== MARDI 23 NOVEMBRE salle 1.124 LIRMM bâtiment 5

• 15h Richard MOOT soutenance d’habilitation à diriger les recherches:
  TYPE-LOGICAL INVESTIGATIONS:
  PROOF-THEORETIC, COMPUTATIONAL AND LINGUISTIC APSECTS OF TYPE LOGICAL GRAMMARS
  Vito Michele ABRUSCI (Univ Roma tre) rapporteur
  David DELAHAYE (LIRMM, Univ Montpellier, CNRS ) examinateur
  Andreas HERZIG (IRIT, Univ Paul Sabatier, CNRS) examinateur
  Gérard HUET (INRIA, Académie des Sciences) rapporteur
  Robert LEVINE (Ohio State University)
  Renihard MUSKENS (ILLC, Amsterdam)
  Myriam QUATRINI (I2M, Aix-Marseille Université) rapporteur
  Christian RETORÉ (LIRMM, Univ Montpellier, CNRS ) examinateur
  Type-logical grammars are a systematic way of using logic for natural language analysis, which puts special emphasis on the syntax-semantics interface. In recent years, many new logical formalisms have been developed for type-logical grammars. In my habilitation, I present two ways to adapt the proof nets of linear logic to these different type-logical grammars. Surprisingly, natural language analyses for calculi with different logical primitives translate, in many cases, into logically equivalent statements when translated to these proof nets. The two proof net frameworks for modern type-logical grammars show that, despite starting for different logical primitives, there is much greater convergence than has previously been assumed. Because the proof system is so general, it has been implemented to serve a single theorem prover engine for multiple grammatical frameworks, hiding, if desired, the linear logic internals from the end user.
  
  
• 18h Davide CATTA Soutenance de thèse 

  DES PREUVES COMME DES JEUX ET RÉCIPROQUEMENT
  APPLICATION À LA SÉMANTIQUE DE LANGAGES NATURELS OU LOGIQUES
Vito Michele ABRUSCI (Univ Roma tre) rapporteur
David DELAHAYE (LIRMM, Univ Montpellier, CNRS ) examinateur
Andreas HERZIG (IRIT, Univ Paul Sabatier, CNRS) rapporteur
Jean-Yves MARION (Univ Lorraine, LORIA) examinateur
Richard MOOT (LIRMM, Univ Montpellier, CNRS ) co-encadrant
Valeria DE PAIVA (Topos Institute, Berkeley) examinatrice
Myriam QUATRINI (I2M, Aix-Marseille Université) co-encadrante
Christian RETORÉ (LIRMM, Univ Montpellier, CNRS ) co-encadrant
Alexis SAURIN (CNRS, PPS INRIA Univ Paris) invité
Dans cette thèse, nous proposons une approche dialogique à la sémantique des langages logiques et à la sémantique des langages naturels, dont nous montrons la complétude pour la logique du premier ordre avec termes. Nos dialogues sont des débats entre un Proposant, qui essaye de construire une justification pour un énoncé, et un Opposant qui essaye de réfuter le même énoncé. Nous montrons que cette type de sémantique argumentative peut s'appliquer à la fois aux formules logique et --- via les grammaires catégorielles --- à des phénomènes linguistiques comme l'anaphore. Dans la même optique nous proposons une sémantique des jeux pour la logique modale K constructive, sémantique qui a la particularité de pouvoir composer des stratégies, tout comme la coupure compose des preuves.

=== MERCREDI 24 NOVEMBRE salle 1.124 LIRMM bâtiment 5

• 10h Vito Michele ABRUSCI (Università di Roma tre)
  LOGIQUE LINÉAIRE ET INTERACTION
  La logique linéaire a largement contribué et contribue encore à focaliser l'attention de la recherche logique sur le thème de l'interaction, thème de nature logique. Dans cet exposé - qui s'adresse également aux non-spécialistes de la logique-  je présenterai les contributions que je crois être parmi les plus importantes, données par la logique linéaire, pour comprendre la présence de l'interaction en logique (en particulier dans les preuves et leurs transformations) et pour avancer dans l'étude générale de l'interaction.
  Pause 5'
  
• 11h Myriam QUATRINI (I2M Aix-Marseille université)
  THÉORIE DE LA DÉMONSTRATION ET FORMALISATION DES DIALOGUES
  Après un bref retour sur l'irruption de la logique linéaire en théorie de la démonstration, nous soulignerons les aspects de cette approche de la logique qui vont être pertinents dans la formulation de la Ludique. Nous présenterons informellement cette théorie logique et illustrerons sur des exemples son intérêt pour la formalisation des dialogues.
  Pause 5'
  
• 12h Andreas HERZIG (CNRS-IRIT, Toulouse, France)
  BELIEF KNOWLEDGE AND COMMON KNOWLEDGE ABOUT A PROPOSITION
  Traditionally epistemic logics focus on the modalities `agent believes that P is true' and `agent knows that P is true', where P is a proposition. Instead, I will examine reasoning with the modalities `agent has belief about P' and `agent has knowledge about P' (the latter being more commonly called `knowledge whether P'). I will show that this perspective leads to new insights about the interplay (1) between belief and knowledge and (2) between knowledge and common knowledge.
• 13h Repas