2026-07-22T06:29:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15752 2024-03-06T10:56:07Z ddc:004 open_access

BV and Pomset Logic Are Not the Same Nguyễn, Lê Thành Dũng (Tito) Straßburger, Lutz proof nets deep inference pomset logic system BV cographs dicographs series-parallel orders 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger 2022 Is Part Of LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2022.32 urn:nbn:de:0030-drops-157521 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.32 eng https://creativecommons.org/licenses/by/4.0/legalcode