License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.25
URN: urn:nbn:de:0030-drops-59805
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5980/
Go to the corresponding LIPIcs Volume Portal

Laurent, Olivier

Focusing in Orthologic

pdf-format:
LIPIcs-FSCD-2016-25.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{laurent:LIPIcs:2016:5980,
  author =	{Olivier Laurent},
  title =	{{Focusing in Orthologic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{25:1--25:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5980},
  URN =		{urn:nbn:de:0030-drops-59805},
  doi =		{10.4230/LIPIcs.FSCD.2016.25},
  annote =	{Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination}
}

Keywords: orthologic, focusing, minimal quantum logic, linear logic, automatic proof search, cut elimination
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI