Intuitionistic BV

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

Abstract

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 34th International Conference, TABLEAUX 2025, Proceedings
EditorsGian Luca Pozzato, Tarmo Uustalu
PublisherSpringer Science and Business Media Deutschland GmbH
Pages414-432
Number of pages19
ISBN (Print)9783032060846
DOIs
Publication statusPublished - 1 Jan 2026
Externally publishedYes
Event34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2025 - Reykjavik, Iceland
Duration: 27 Sept 202529 Sept 2025

Publication series

NameLecture Notes in Computer Science
Volume15980 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2025
Country/TerritoryIceland
CityReykjavik
Period27/09/2529/09/25

Fingerprint

Dive into the research topics of 'Intuitionistic BV'. Together they form a unique fingerprint.

Cite this