MARDI
23 NOVEMBRE 2021 APRES-MIDI
MERCREDI
24 NOVEMBRE MATIN
JOURNEE(S)
LOGIQUE ET INTERACTION
dans le cadre des actions transverses du LIRMM
Lien
pour l'inscription à remplir au vu des restrictions sanitaires
.......et pour prévoir les repas du mercredi 24 midi.
=== 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
Lien
pour l'inscription à remplir au vu des restrictions sanitaires
.......et pour prévoir les repas du mercredi 24 midi.