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

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

Publikováno v: Logical Methods in Computer Science, Vol Volume 19, Issue 4 (2023)

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 fro

Externí odkaz: https://doaj.org/article/2c50f3cefe774fb1ba90006df8bf47dc

On linear rewriting systems for Boolean logic and some applications to proof theory

Autor: Anupam Das, Lutz Straßburger

Publikováno v: Logical Methods in Computer Science, Vol Volume 12, Issue 4 (2017)

Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written

Externí odkaz: https://doaj.org/article/2fdcd8809e30471b89df06d0ffd814b5

Herbrand-Confluence

Autor: Stefan Hetzl, Lutz Straßburger

Publikováno v: Logical Methods in Computer Science, Vol Volume 9, Issue 4 (2013)

We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and mathematically more r

Externí odkaz: https://doaj.org/article/4d39ecc186364a339c0563779d3af15b

Game Semantics for Constructive Modal Logic

Autor: Davide Catta, Lutz Straßburger, Matteo Acclavio

Publikováno v: Lecture Notes in Computer Science
TABLEAUX 2021-30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
TABLEAUX 2021-30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2021, Birmingham, United Kingdom. pp.428-445, ⟨10.1007/978-3-030-86059-2_25⟩
Lecture Notes in Computer Science ISBN: 9783030860585
TABLEAUX
Automated Reasoning with Analytic Tableaux and Related Methods
Automated Reasoning with Analytic Tableaux and Related Methods, 12842, Springer International Publishing, pp.428-445, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-86059-2_25⟩

International audience; In this paper we provide the first game semantics for the constructive modal logic CK. We first define arenas encoding modal formulas, we then define winning innocent strategies for games on these arenas, and finally we charac

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::444e304d416c61bc37bed2e16f0350ed
https://inria.hal.science/hal-03369819

Combinatorial Proofs and Decomposition Theorems for First-order Logic

Autor: Jui-Hsuan Wu, Dominic J. D. Hughes, Lutz Straßburger

Publikováno v: LICS
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩

We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a syntax-free

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c06f8822791a98127c3f2cf9572a688
http://arxiv.org/abs/2104.13124