BV and Pomset Logic Are Not the Same

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publication30th EACSL Annual Conference on Computer Science Logic, CSL 2022
EditorsFlorin Manea, Alex Simpson
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772181
DOIs
Publication statusPublished - 1 Feb 2022
Event30th EACSL Annual Conference on Computer Science Logic, CSL 2022 - Virtual, Gottingen, Germany
Duration: 14 Feb 202219 Feb 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume216
ISSN (Print)1868-8969

Conference

Conference30th EACSL Annual Conference on Computer Science Logic, CSL 2022
Country/TerritoryGermany
CityVirtual, Gottingen
Period14/02/2219/02/22

Keywords

  • Cographs
  • Deep inference
  • Dicographs
  • Pomset logic
  • Proof nets
  • Series-parallel orders
  • System BV

Fingerprint

Dive into the research topics of 'BV and Pomset Logic Are Not the Same'. Together they form a unique fingerprint.

Cite this