Document Open Access Logo

Focusing in Orthologic

Author Olivier Laurent

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.25.pdf
  • Filesize: 0.51 MB
  • 17 pages

Document Identifiers

Author Details

Olivier Laurent

Cite As Get BibTex

Olivier Laurent. Focusing in Orthologic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.25

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 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.

Subject Classification

Keywords
  • orthologic
  • focusing
  • minimal quantum logic
  • linear logic
  • automatic proof search
  • cut elimination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297-347, 1992. Google Scholar
  2. Garrett Birkhoff. Lattice Theory, volume 25 of Colloquium Publications. American Mathematical Society, third edition, 1967. Google Scholar
  3. Günter Bruns. Free ortholattices. Canadian Journal of Mathematics, 28(5):977-985, October 1976. Google Scholar
  4. 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. Google Scholar
  5. Uwe Egly and Hans Tompits. On different proof-search strategies for orthologic. Studia Logica, 73(1):131-152, February 2003. Google Scholar
  6. 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. Google Scholar
  7. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  8. Jean-Yves Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3):255-296, 1991. Google Scholar
  9. Robert Goldblatt. Semantic analysis of orthologic. Journal of Philosophical Logic, 3(1-2):19-35, 1974. Google Scholar
  10. Robert Goldblatt. Orthomodularity is not elementary. Journal of Symbolic Logic, 49(2):401-404, 1984. Google Scholar
  11. Olivier Laurent. A proof of the focalization property of linear logic. Unpublished note, May 2004. Google Scholar
  12. William McCune. Automatic proofs and counterexamples for some ortholattice identities. Information Processing Letters, 65(6):285-291, 1998. Google Scholar
  13. Hirokazu Nishimura. Proof theory for minimal quantum logic I. International Journal of Theoretical Physics, 33(1):103-113, January 1994. Google Scholar
  14. Jürgen Schulte Mönting. Cut elimination and word problems for varieties of lattices. Algebra Universalis, 12:290-321, December 1981. Google Scholar
  15. Philip Whitman. Free lattices. Annals of Mathematics, 42(1):325-330, January 1941. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact