  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
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 to optimise proof search. We demonstrate how to take
benefits from the new systems in automatic proof search for orthologic.
