vendredi 22 janvier 2021 LIRMM + online

10:00 - Handsome proof nets

Christian RETORE (Université de Montpellier, LIRMM)

Handsome proof nets identify equivalent proofs as much as possible --- order of rules, commutativity and associativity of the connectives. They are simply defined as and edge bicoloured graph over atoms, consisting in a Red cograph decipting the conclusion formula and a Blue perfect matching of the whole graph. The correctness criterion is quite simple: for every cycle alternating Red and Blue edges the R and B graph contains at lest a chord. Cut elimination results from the fact that some graph rewriting rules preserve correctness. So far, this view of proof nets is the only one to apply to pomset logic, a non commutative extension of classical logic issued form coherence semantics.

10:30 TBA

Thomas ERHARD (Université Paris 7)

11:15 - A complexity gap between pomset logic and system BV ( joint work with Lutz Strassburger)

Lê Thành Dũng NGUYEN (Université Sorbonne Paris nord, LIPN)

Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective which is self-dual and non-commutative. The former uses proof nets while the latter was the first exampke of a deep inference system. It has long been conjectured that these two logics are the same. We show that non only this conjecture is false - there is an explicit counter example - but there is a fundamental complexity-theoretic reason for this: provability is a stricly harder problem in pomset logic than in BV unless NP=coNP.

11:45 - Fantastic connectives and Where to Find Them

Matteo ACCLAVIO (Luxembourg University)

Fantastic connectives and Where to Find Them represents the fruit of many years' travel and research. [...] The definition of a 'generalised connectives' has caused controversy for decades. Though this might surprise some first-time students of logic, the problem might come into clear focus if we take a moment to consider three types of generalised connectives: synthetic connectives, connectives-as-partitions and connectives-as-graphs. [...] We now ask ourselves: which of these creatures is a 'being' -- that is to say, a creature worthy of legal rights and voice in logic -- and which is a 'beast'? [...] Jean-Yves Girard, the founder of Linear Logic, decreed that any connective which admits a linear and context-free introduction rule, would henceforth be granted the status of 'multiplicative connective'. [...] As we see, the mere possession of such a rule, was no guarantee that a connectives could or would well-behave with respect to cut-elimination. In a recent joint work with Ross Horne and Lutz Strassburger, we define 'connectives-as-graphs' in the hope of creating closer ties between multiplicative linear logic and our graphical proof system GS. [...] Let us now turn on the one question that linear logicians ask more than any other when the conversation turns to our connectives: why do you say that these objects describe new connectives? ( This talk is based on https://arxiv.org/abs/2012.01102 and https://drops.dagstuhl.de/opus/volltexte/2020/11649/pdf/LIPIcs-CSL-2020-6.pdf )

12:15- Lunch break

13:30 - Proof nets: representation of syllogisms, representation of law of categorial grammar

Vito Michele ABRUSCI (Università Roma tre)

I will show and discuss how to represent in terms of (non commutative) proof-nets:

- the syllogisms considered in ancient, medieval and modern logic;

- the laws of categorial grammar.

14:00 - Strong Normalization of Elementary Proof-Nets

Olivier LAURENT (ENS Lyon)

We present a proof of strong normalization of proof-nets for elementary linear logic. It follows the simple pattern of assigning an ordinal to each proof-net, and proving that this ordinal value decreases under any reduction step. As it is often the case with light logic systems, types play no role and only the geometry (i.e. paths) of the proof-net matters.

14:30 - A reading of Girard's Transcendental Syntax

Boris ENG (Université Sorbonne Paris nord, LIPN)

Following the Geometry of Interaction programme, Girard's Transcendental Syntax gives the outline of a finitary, homogeneous and interactive architecture of logic based on computation. Thomas Seiller and I suggest an attempt at a first technical development of this programme. As a first step, we encode multiplicative proof-structures into the Stellar Resolution, a model of computation based on Robinson's first-order resolution. We then show how cut-elimination and logical correctness can be naturally expressed as a non-deterministic resolution of constraints on addresses refering to the physical locations of a proof-structure.