A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

DOI10.46298/LMCS-19(4:25)2023arXiv2209.07825OpenAlexW4312076504MaRDI QIDQ6137849FDOQ6137849

Authors: Lê Thành Dũng Nguyên, Lutz Straßburger 

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs, and proof systems. Both logics enjoy a cut-admissibility result, but for neither logic can this be done in the sequent calculus. Provability in pomset logic can be checked via a proof net correctness criterion and in BV via a deep inference proof system. It has long been conjectured that these two logics are the same. In this paper we show that this conjecture is false. We also investigate the complexity of the two logics, exhibiting a huge gap between the two. Whereas provability in BV is NP-complete, provability in pomset logic is $Sigm{a}_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.

Full work available at URL: https://arxiv.org/abs/2209.07825

zbMATH Keywords

proof netscographsdeep inferenceseries-parallel ordersrelation websdicographsPomset logicsystem \textsf{BV}

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Computational Complexity
• Complement reducible graphs
• The Logic of Bunched Implications
• Linear logic
• Extension without cut
• Quantales and (noncommutative) linear logic
• The Recognition of Series Parallel Digraphs
• The logic of categorial grammars. A deductive account of natural language syntax and semantics
• The relative efficiency of propositional proof systems
• A complete axiomatisation for the inclusion of series-parallel partial orders
• The Mathematics of Sentence Structure
• The mix rule
• Fully dynamic recognition algorithm and certificate for directed cographs
• Title not available (Why is that?)
• Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics
• Title not available (Why is that?)
• The structure of multiplicatives
• A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
• Acyclicity and Coherence in Multiplicative Exponential Linear Logic
• Visible acyclic differential nets. I: Semantics
• A semantic characterisation of the correctness of a proof net
• Complete sets and the polynomial-time hierarchy
• A Local System for Classical Logic
• A system of interaction and structure
• Title not available (Why is that?)
• Deep inference and probabilistic coherence spaces
• A System of Interaction and Structure II: The Need for Deep Inference
• Simple free star-autonomous categories and full coherence
• Non-commutative logic. I: The multiplicative fragment
• Complexity of trails, paths and circuits in arc-colored digraphs
• Title not available (Why is that?)
• Classes of Directed Graphs
• On noncommutative extensions of linear logic
• Computer Science Logic
• Handsome proof-nets: Perfect matchings and cographs
• Computer Science Logic
• A term equality problem equivalent to graph isomorphism
• A system of interaction and structure IV
• Non-commutative logic II: sequent calculus and phase semantics
• System BV is NP-complete
• A system of interaction and structure. V: The exponentials and splitting
• System NEL is Undecidable
• Title not available (Why is that?)
• A Logical Basis for Quantum Evolution and Entanglement
• Proof nets for multiplicative cyclic linear logic and Lambek calculus
• Ribbon Tensorial Logic
• The Consistency and Complexity of Multiplicative Additive System Virtual
• A correspondence between rooted planar maps and normal planar lambda terms
• An Analytic Propositional Proof System on Graphs
• Logic Beyond Formulas
• Generalized connectives for multiplicative linear logic
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• Linear logic model of state revisited
• Title not available (Why is that?)
• Pomset Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructing weak simulations from linear implications for processes with private names
• BV and Pomset Logic Are Not the Same
• A deep inference system with a self-dual binder which is complete for linear lambda calculus

This page was built for publication: A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137849)