Subexponentials in non-commutative linear logic
From MaRDI portal
Publication:5236554
DOI10.1017/S0960129518000117zbMATH Open1456.03099arXiv1709.03607OpenAlexW3105030000WikidataQ129899229 ScholiaQ129899229MaRDI QIDQ5236554FDOQ5236554
Stepan Kuznetsov, Andre Scedrov, Max Kanovich, Vivek Nigam
Publication date: 9 October 2019
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Abstract: Linear logical frameworks with subexponentials have been used for the specification of among other systems, proof systems, concurrent programming languages and linear authorization logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organized as sets and multisets of formulae not being possible to organize formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut-elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.
Full work available at URL: https://arxiv.org/abs/1709.03607
Recommendations
Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Cites Work
- Decision problems for propositional linear logic
- Lambek calculus is NP-complete
- Relationships between nondeterministic and deterministic tape complexities
- Linear logic
- Logic programming in a fragment of intuitionistic linear logic
- A General Proof System for Modalities in Concurrent Constraint Programming
- On the Complexity of Linear Authorization Logics
- Quantales and (noncommutative) linear logic
- Title not available (Why is that?)
- The logic of categorial grammars. A deductive account of natural language syntax and semantics
- The Mathematics of Sentence Structure
- Recursive Unsolvability of a problem of Thue
- Title not available (Why is that?)
- The Lambek calculus enriched with additional connectives
- Some Decision Problems in the Theory of Syntactic Categories
- Logic Programming with Focusing Proofs in Linear Logic
- Language in action. Categories, lambdas and dynamic logic
- Title not available (Why is that?)
- Multimodal linguistic inference
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Forum: A multiple-conclusion specification logic
- On translating Lambek grammars with one division into context-free grammars
- Some Syntactical Observations on Linear Logic
- Title not available (Why is that?)
- A comparison between lambek syntactic calculus and intuitionistic linear propositional logic
- Subexponential concurrent constraint programming
- Undecidability of the Lambek calculus with subexponential and bracket modalities
- An extended framework for specifying and reasoning about proof systems
- Classical and Intuitionistic Subexponential Logics Are Equally Expressive
- Undecidability of the Lambek Calculus with a Relevant Modality
- Title not available (Why is that?)
- On Lambek’s Restriction in the Presence of Exponential Modalities
- A framework for linear authorization logics
- Title not available (Why is that?)
- Lambek calculus with a unit and one division
Cited In (18)
- A fresh view of linear logic as a logical framework
- A linear logic framework for multimodal logics
- Versions of a local contraction subexponential in the Lambek calculus
- Relational Models for the Lambek Calculus with Intersection and Constants
- Soft subexponentials and multiplexing
- The multiplicative-additive Lambek calculus with subexponential and bracket modalities
- Universal proof theory: semi-analytic rules and Craig interpolation
- Explorations in Subexponential Non-associative Non-commutative Linear Logic
- Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic
- Complexity of Lambek calculi with modalities and of total derivability in grammars
- Infinitary action logic with exponentiation
- Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
- On noncommutative extensions of linear logic
- Non-associative, non-commutative multi-modal linear logic
- Kleene star, subexponentials without contraction, and infinite computations
- Infinitary action logic with multiplexing
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Title not available (Why is that?)
Uses Software
This page was built for publication: Subexponentials in non-commutative linear logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5236554)
