View article

We present a new phased sequent calculus PBI for a subset of BI, BIsub, where multiplicative implications and multiplicative units do not occur. It is a sequent calculus which recognizes two distinct phases which alternate during derivation. A set of inference rules is defined for each of them, facilitating modularity in sequent calculus. With PBI, it is not a laborious task to show the termination property of a BIsub backward proof search. In fact, the modularity of the calculus allows a very succinct termination proof. We conclude by showing that PBI is equivalent to LBIsub: LBI restricted to BIsub connectives.