 |
 |
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)2017Focusing in OrthologicArticle
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: 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
Funding:
- Source : OpenAIRE Graph
- Funder: French National Research Agency (ANR); Code: ANR-10-LABX-0070
- Expanding Logical Ideas for Complexity Analysis; Funder: French National Research Agency (ANR); Code: ANR-14-CE25-0005
- Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-BS02-0010
- Realizability for classical logic, concurrency, references and rewriting; Funder: French National Research Agency (ANR); Code: ANR-11-IDEX-0007
Classifications
Mathematics Subject Classification 20201
- 03B35 - Mechanization of proofs and logical operations
- 03B47 - Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
- 03F05 - Cut-elimination and normal-form theorems
- 03F52 - Proof-theoretic aspects of linear logic and other substructural logics
- 03G12 - Quantum logic
- 68V15 - Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
1 Document citing this article
Consultation statistics
This page has been seen 2306 times.
This article's PDF has been downloaded 333 times.