Focusing in orthologic

DOI10.23638/LMCS-13(3:6)2017MaRDI QIDQ5367044zbMATH OpenFDO

Authors Olivier Laurent

Publication date 12 October 2017

Full work available at URL https://arxiv.org/abs/1612.01728

zbMATH Keywords

automatic proof searchcut eliminationfocusinglinear logicminimal quantum logicorthologic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Quantum logic (03G12) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

Recommendations

• Focusing in Orthologic
• On different proof-search strategies for orthologic
• Labeled Sequent Calculus for Orthologic
• From basic logic to quantum logics with cut-elimination
• The focused calculus of structures

Cited in

(5)

• From basic logic to quantum logics with cut-elimination
• On different proof-search strategies for orthologic
• Proof theory for minimal quantum logic: A remark
• Focusing in Orthologic
• Sequent Calculi for Orthologic with Strict Implication

This page was built for publication: Focusing in orthologic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5367044)