TL;DR
This paper introduces new sequent calculus systems for orthologic that incorporate focusing techniques to improve proof search efficiency, while maintaining cut elimination.
Contribution
It presents two novel sequent calculus systems for orthologic, one leveraging involutive negation and the other integrating focusing to optimize proof search.
Findings
New sequent calculus systems for orthologic with cut elimination
Focusing improves proof search efficiency in orthologic
Demonstrated benefits in automatic proof search algorithms
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.