摘要：Development of a contraction-free BI sequent calculus, be the contraction-freeness implicit or explicit, has not been successful in the literature. We address this problem by presenting such a sequent system. Our calculus involves no structural rules. It should be an insight into non-formula contraction absorption in other non-classical logics. Contraction absorption in sequent calculus is associated to simpler cut elimination and to efficient proof searches.
