Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus

Ryuta Arisaka (1)

1 PARSIFAL - Proof search and reasoning with logic specifications

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.

Mots clés: proof theory; BI; sequent calculus; contraction-free; cut elimination

Domaines: Logique en informatique [cs.LO]

Ryuta Arisaka. Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. 2014. ⟨hal-00982331⟩