Rauszer's bi-intuitionistic propositional logic (BiInt) is the conservative extension of intuitionistic propositional logic (Int) with a connective dual to implication usually called 'exclusion'. A *standard-style* sequent calculus for BiInt is easily obtained by extending the multiple-conclusion sequent calculus of Int with exclusion rules dual to the implication rules. However, similarly to standard-style sequent calculi for modal logics like S5, this calculus is incomplete without the cut rule. Cut-freeness is achievable for sequent calculi with non-standard sequent forms. The *nested* and *labelled* calculi (Goré, Postniece; Pinto, Uustalu) were motivated by quite different intuitive considerations. Yet they turn out to be very close on the technical level: slightly adjusted towards each other, they can be made isomorphic.

This is joint work with Luís Pinto (Universidade do Minho).