Lê Thành Dũng Nguyên ; Lutz Straßburger - A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

lmcs:10057 - Logical Methods in Computer Science, December 18, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:25)2023
A System of Interaction and Structure III: The Complexity of BV and Pomset LogicArticle

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

    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 $\Sigma_2^p$-complete. We also make some observations with respect to possible sequent systems for the two logics.


    Volume: Volume 19, Issue 4
    Published on: December 18, 2023
    Accepted on: October 13, 2023
    Submitted on: September 19, 2022
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • a cartographic quest between lambda-calculus, logic, and combinatorics; Funder: French National Research Agency (ANR); Code: ANR-21-CE48-0017
    • Community of mathematics and fundamental computer science in Lyon; Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070

    Consultation statistics

    This page has been seen 715 times.
    This article's PDF has been downloaded 133 times.