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

DOI10.46298/LMCS-19(4:25)2023MaRDI QIDQ6137849OpenAlexFDO

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)

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)

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.

Recommendations

• BV and Pomset Logic Are Not the Same
• On noncommutative extensions of linear logic
• Pomset logic. The other approach to noncommutativity in logic
• scientific article; zbMATH DE number 2185722
• System BV is NP-complete

Cites work

• scientific article; zbMATH DE number 2185722 (Why is no real title available?)
• scientific article; zbMATH DE number 4099289 (Why is no real title available?)
• scientific article; zbMATH DE number 1841813 (Why is no real title available?)
• scientific article; zbMATH DE number 2090535 (Why is no real title available?)
• scientific article; zbMATH DE number 6157240 (Why is no real title available?)
• scientific article; zbMATH DE number 7559871 (Why is no real title available?)
• scientific article; zbMATH DE number 7199586 (Why is no real title available?)
• A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
• A Local System for Classical Logic
• A System of Interaction and Structure II: The Need for Deep Inference
• A complete axiomatisation for the inclusion of series-parallel partial orders
• A correspondence between rooted planar maps and normal planar lambda terms
• A deep inference system with a self-dual binder which is complete for linear lambda calculus
• A logical basis for quantum evolution and entanglement
• A semantic characterisation of the correctness of a proof net
• A system of interaction and structure
• A system of interaction and structure. IV: The exponentials and decomposition
• A system of interaction and structure. V: The exponentials and splitting
• A term equality problem equivalent to graph isomorphism
• Acyclicity and Coherence in Multiplicative Exponential Linear Logic
• An Analytic Propositional Proof System on Graphs
• BV and Pomset Logic Are Not the Same
• Classes of directed graphs
• Coherent interaction graphs
• Complement reducible graphs
• Complete sets and the polynomial-time hierarchy
• Complexity of trails, paths and circuits in arc-colored digraphs
• Computational Complexity
• Computer Science Logic
• Computer Science Logic
• Constructing weak simulations from linear implications for processes with private names
• De Morgan dual nominal quantifiers modelling private names in non-commutative logic
• Deep inference and probabilistic coherence spaces
• Extension without cut
• Fully dynamic recognition algorithm and certificate for directed cographs
• Generalized connectives for multiplicative linear logic
• Handsome proof-nets: Perfect matchings and cographs
• Linear logic
• Linear logic model of state revisited
• Logic beyond formulas: a proof system on graphs
• Non-commutative logic II: sequent calculus and phase semantics
• Non-commutative logic. I: The multiplicative fragment
• On noncommutative extensions of linear logic
• Pomset logic. The other approach to noncommutativity in logic
• Proof nets for multiplicative cyclic linear logic and Lambek calculus
• Quantales and (noncommutative) linear logic
• Ribbon tensorial logic
• Simple free star-autonomous categories and full coherence
• System BV is NP-complete
• System NEL is undecidable
• Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics
• The Logic of Bunched Implications
• The Mathematics of Sentence Structure
• The Recognition of Series Parallel Digraphs
• The consistency and complexity of multiplicative additive system virtual
• The logic of categorial grammars. A deductive account of natural language syntax and semantics
• The mix rule
• The relative efficiency of propositional proof systems
• The structure of multiplicatives
• Visible acyclic differential nets. I: Semantics

Cited in

(2)

• A graphical proof theory of logical time
• BV and Pomset Logic Are Not the Same

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)