  In this paper, we present a propositional sequent calculus containing
disjoint copies of classical and intuitionistic logics. We prove a
cut-elimination theorem and we establish a relation between this system and
linear logic.
