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.

Comment: Small rewritings. Updated benchmark section. Updated coq and ocaml files

• 03B35 - Mechanization of proofs and logical operations
• 03B47 - Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
• 03F05 - Cut-elimination and normal-form theorems
• 03F52 - Proof-theoretic aspects of linear logic and other substructural logics
• 03G12 - Quantum logic
• 68V15 - Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)