BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:8836@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20251009T110000
DTEND;TZID=Europe/Paris:20251009T123000
DTSTAMP:20251211T072517Z
URL:https://www.i2m.univ-amu.fr/evenements/cut-expansion-in-proof-nets-of-
 multiplicative-linear-logic/
SUMMARY:Rémi Di Guardia (IRIF\, Paris Cité): Cut-Expansion in Proof-Nets 
 of Multiplicative Linear Logic
DESCRIPTION:Rémi Di Guardia: Cut-elimination is a rewriting system defined
  in many logics\, which has been widely studied. In general\, a major resu
 lt is to prove its weak normalization\, which implies a provable formula a
 lways admits a cut-free proof. From this\, various results can be more eas
 ily deduced: for instance that there is no proof of false. However\, the r
 everse procedure - that we call cut-expansion - has been much less studied
  even though it is also useful! A goal here is the following: given a proo
 f π with many cuts\, can we find a proof π' with exactly one cut at its 
 root and that reduces to π? Such a result has two applications. First\, i
 t allows to find a Kraig's interpolant in the spirit of [Sau25\,FOS25]. It
  is also useful in the case of a denotational semantic: while it is often 
 clear how to interpret a single cut-rule between two proofs\, it may not b
 e the case for two proofs linked by "a bunch" of cut-rules - this problem 
 was encountered e.g. in [EFP24].\nWe will present a very simple proof on h
 ow to apply cut-expansion steps to obtain only one cut-rule from a proof w
 ith many cut-rules in Multiplicative Linear Logic. We do so in the proof-n
 et syntax as the proof is really easy to intuit in this formalism. We then
  use this result to immediately get a proof of Kraig's interpolation. Last
 ly\, and if time allows\, we sketch how to extend our proof to full linear
  logic.\n\n[Sau25] Alexis Saurin. Interpolation as Cut-Introduction: On th
 e Computational Content of Craig-Lyndon Interpolation. FSCD 2025. https://
 doi.org/10.4230/LIPIcs.FSCD.2025.32\n[FOS25] Guido Fiorillo\, Daniel Osori
 o Valencia\, and Alexis Saurin. On Correctness\, Sequentialization and Int
 erpolation. TLLA 2025.\n[EFP24] Thomas Ehrhard\, Claudia Faggian\, and Mic
 hele Pagani. Bayesian Networks and Proof-Nets: a proof-theoretical account
  of Bayesian Inference. Technical Report. https://doi.org/10.48550/arXiv.2
 412.20540
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - TPR2\, Salle de Séminaire 304-306 (3ème étage)\, 1
 63 Avenue de Luminy\, Marseille\, 13009\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, Mars
 eille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - TPR2\, Sall
 e de Séminaire 304-306 (3ème étage):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20250330T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR