Laurent, Olivier - Focusing in Orthologic

lmcs:3808 - Logical Methods in Computer Science, July 21, 2017, Volume 13, Issue 3
Focusing in Orthologic

Authors: Laurent, Olivier

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.


Source : oai:arXiv.org:1612.01728
DOI : 10.23638/LMCS-13(3:6)2017
Volume: Volume 13, Issue 3
Published on: July 21, 2017
Submitted on: July 21, 2017
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1


Share

Browsing statistics

This page has been seen 67 times.
This article's PDF has been downloaded 14 times.