Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

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.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00982331
Author Arisaka, Ryuta
Maintainer CCSD
Last Updated May 5, 2026, 13:33 (UTC)
Created May 5, 2026, 13:33 (UTC)
Identifier hal-00982331
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Proof search and reasoning with logic specifications (PARSIFAL) ; Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX) ; École polytechnique (X) ; Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X) ; Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)-Centre Inria de Saclay ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
creator Arisaka, Ryuta
date 2014-04-23T00:00:00
harvest_object_id 0a98b80a-bdf2-4c95-8622-75ff6d98425f
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-08-20T00:00:00
relation info:eu-repo/semantics/altIdentifier/arxiv/1404.6037
set_spec type:UNDEFINED