BV and Pomset Logic Are Not the Same
| Autor: | Nguy���n, L�� Th��nh D��ng (Tito), Stra��burger, Lutz |
|---|---|
| Přispěvatelé: | Preuves et Langages (PLUME), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
2012 ACM Subject Classification Theory of computation → Linear logic
system BV dicographs [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] series-parallel orders Digital Object Identifier 10.4230/LIPIcs.CSL.2022.32 proof nets cographs Theory of computation ��� Linear logic Theory of computation → Proof theory phrases proof nets Theory of computation → Proof theory phrases proof nets deep inference pomset logic system BV cographs dicographs series-parallel orders Digital Object Identifier 10.4230/LIPIcs.CSL.2022.32 series-parallel orders Theory of computation ��� Proof theory Computer Science::Logic in Computer Science deep inference pomset logic |
| Zdroj: | CSL 2022-30th EACSL Annual Conference on Computer Science Logic CSL 2022-30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.32⟩ 30th EACSL Annual Conference on Computer Science Logic, CSL 2022 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.32⟩ |
| DOI: | 10.4230/LIPIcs.CSL.2022.32⟩ |
| Popis: | BV and pomset logic are two logics that both conservatively extend unit-free multiplicative linear logic by a third binary connective, which (i) is non-commutative, (ii) is self-dual, and (iii) lies between the "par" and the "tensor". It was conjectured early on (more than 20 years ago), that these two logics, that share the same language, that both admit cut elimination, and whose connectives have essentially the same properties, are in fact the same. In this paper we show that this is not the case. We present a formula that is provable in pomset logic but not in BV. LIPIcs, Vol. 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), pages 32:1-32:17 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|