Focusing in Orthologic
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.
orthologic
focusing
minimal quantum logic
linear logic
automatic proof search
cut elimination
25:1-25:17
Regular Paper
Olivier
Laurent
Olivier Laurent
10.4230/LIPIcs.FSCD.2016.25
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992.
Garrett Birkhoff. Lattice Theory, volume 25 of Colloquium Publications. American Mathematical Society, third edition, 1967.
Günter Bruns. Free ortholattices. Canadian Journal of Mathematics, 28(5):977-985, October 1976.
Uwe Egly and Hans Tompits. Gentzen-like methods in quantum logic. Technical Report 99-1, Institute for Programming and Logics, University at Albany - SUNY, 1999. Position Papers of TABLEAUX '99.
Uwe Egly and Hans Tompits. On different proof-search strategies for orthologic. Studia Logica, 73(1):131-152, February 2003.
Claudia Faggian and Giovanni Sambin. From basic logic to quantum logics with cut-elimination. International Journal of Theoretical Physics, 37(1):31-37, January 1998.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987.
Jean-Yves Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3):255-296, 1991.
Robert Goldblatt. Semantic analysis of orthologic. Journal of Philosophical Logic, 3(1-2):19-35, 1974.
Robert Goldblatt. Orthomodularity is not elementary. Journal of Symbolic Logic, 49(2):401-404, 1984.
Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004.
William McCune. Automatic proofs and counterexamples for some ortholattice identities. Information Processing Letters, 65(6):285-291, 1998.
Hirokazu Nishimura. Proof theory for minimal quantum logic I. International Journal of Theoretical Physics, 33(1):103-113, January 1994.
Jürgen Schulte Mönting. Cut elimination and word problems for varieties of lattices. Algebra Universalis, 12:290-321, December 1981.
Philip Whitman. Free lattices. Annals of Mathematics, 42(1):325-330, January 1941.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode