Olivier Laurent - Focusing in Orthologic

lmcs:2591 - Logical Methods in Computer Science, July 21, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:6)2017
Focusing in OrthologicArticle

Authors: Olivier Laurent

    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.

    https://doi.org/10.23638/LMCS-13(3:6)2017
    Source: arXiv.org:1612.01728
    Volume: Volume 13, Issue 3
    Published on: July 21, 2017
    Accepted on: May 17, 2017
    Submitted on: July 21, 2017
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1
    Licence: arXiv.org - Non-exclusive license to distribute
    Funding:
      Source : OpenAIRE Graph
    • Community of mathematics and fundamental computer science in Lyon; Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070
    • Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-BS02-0010
    • Expanding Logical Ideas for Complexity Analysis; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0005
    • PROJET AVENIR LYON SAINT-ETIENNE; Funder: French National Research Agency (ANR); Code: ANR-11-IDEX-0007

    Publications

    Is part of
    LIPIcs, Volume 52, FSCD'16, Complete Volume
    • 1 ScholeXplorer

    Share and export

    Consultation statistics

    This page has been seen 1160 times.
    This article's PDF has been downloaded 226 times.