Non-commutative logic. III: Focusing proofs.
type: Item
instance of: scholarly article
title: Non-commutative logic. III: Focusing proofs.
zbMATH Open document ID: 1072.03035
DOI: 10.1016/S0890-5401(03)00084-1
author: Roberto Maieli
author: Paul Ruet
published in: Information and Computation
publication date: 2004-03-14T00:00:00Z
review text: The paper studies the focalization property in the framework of \textit{V. M. Abrusci} and \textit{P. Ruet}'s non-commutative logic [Ann. Pure Appl. Logic 101, 29--64 (2000; Zbl 0962.03054)]. Abrusci and Ruet introduced sequent calculus and proof-nets for multiplicative non-commutative logic (MNL), and later \textit{P. Ruet} [Math. Struct. Comput. Sci. 10, 277--312 (2000; Zbl 0999.03056)] extended the sequent calculus to full propositional non-commutative logic (NL). In this paper, the authors define a focalized sequent calculus for NL. The main problem to overcome is related to the extra structure (the order variety) of NL: does it fit in with the (now standard) splitting of connectives into reversible/irreversible? It is shown that one can ``push'' the entropy rule of NL towards the rules of conjunction, and thus give a positive answer. A nice thing is how completeness of the focalized system is proven for MNL: it is shown that every MNL proof-net can be sequentialized into a focalized sequent calculus proof. In the general NL case, completeness is achieved thanks to a careful study of the permutability of the rules.
reviewed by: Lorenzo Tortora de Falco
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 2056067
zbMATH Keywords: focalization
zbMATH Keywords: order varieties
zbMATH Keywords: linear logic
zbMATH Keywords: sequent calculus
MaRDI profile type: Publication
cites work: Non-commutative logic. I: The multiplicative fragment
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: Q4938434
cites work: Q3357521
cites work: On proof normalization in linear logic
cites work: Linear logic
cites work: The Mathematics of Sentence Structure
cites work: Uniform proofs as a foundation for logic programming
cites work: Q4918387
cites work: Non-commutative logic II: sequent calculus and phase semantics
cites work: Quantales and (noncommutative) linear logic
full work available at URL: s0890-5401(03)00084-1
OpenAlex ID: W2127636312
description: scientific article; zbMATH DE number 2056067