Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

TL;DR

This paper introduces a new contraction-free BI sequent calculus that eliminates structural rules, addressing a longstanding open problem in the field.

Contribution

It presents the first successful contraction-free BI sequent calculus, advancing the theoretical understanding of structural rule interactions.

Findings

Developed a contraction-free BI sequent calculus

Eliminated the need for structural rules in the system

Addresses an open problem in the literature

Abstract

Development of a contraction-free BI sequent calculus, be it in the sense of G3i or G4i, has not been successful in literature. We address the open problem by presenting such a sequent system. In fact our calculus involves no structural rules.