We propose new sequent calculus systems for orthologic (also

known as minimal quantum logic) which satisfy the cut

elimination property. The first one is a very simple system relying on

the involutive status of negation. The second one incorporates the

notion of focusing (coming from linear logic) to add

constraints on proofs and thus to facilitate proof search. We

demonstrate how to take benefits from the new systems in automatic

proof search for orthologic.