Speaker:  Matteo Acclavio (SAMOVAR  Telecom SudParis, INRIA  Saclay, LIX  Ecole Polytechnique)


Quando:  21/02/2020  11:30


Dove:  Dipartimento di Matematica e Fisica, Aula 311, Palazzina C


Abstract
There is a wellknown correspondence between formulas and cographs, which are unoriented graphs containing no chordless paths of length 3. The aim of this talk is to shape a proof system operating on general graphs instead of formulas. In such a proof system, we lose the tree structure of formulas corresponding to cographs. As a consequence, we can no longer use the standard proof theoretical methods relying on the tree structure of formulas: for instance, we are not able to identify the main connective of a formula. Thanks to graphs modular decomposition and some techniques from deep inference, we are able to define a proof system with admissible cut rule and which is a conservative extension of MLL with mix. This talk is based on a joint work with Ross Horne and Lutz Strassburger. 