Subexponentials in non-commutative linear logic
From MaRDI portal
Publication:5236554
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3179944 (Why is no real title available?)
- scientific article; zbMATH DE number 1222927 (Why is no real title available?)
- scientific article; zbMATH DE number 1223617 (Why is no real title available?)
- scientific article; zbMATH DE number 517072 (Why is no real title available?)
- scientific article; zbMATH DE number 1406803 (Why is no real title available?)
- scientific article; zbMATH DE number 3251420 (Why is no real title available?)
- scientific article; zbMATH DE number 3316072 (Why is no real title available?)
- scientific article; zbMATH DE number 3045417 (Why is no real title available?)
- A comparison between lambek syntactic calculus and intuitionistic linear propositional logic
- A framework for linear authorization logics
- A general proof system for modalities in concurrent constraint programming
- An extended framework for specifying and reasoning about proof systems
- Classical and intuitionistic subexponential logics are equally expressive
- Conjunctive categorial grammars
- Decision problems for propositional linear logic
- Forum: A multiple-conclusion specification logic
- Lambek calculus is NP-complete
- Lambek calculus with a unit and one division
- Language in action. Categories, lambdas and dynamic logic
- Linear logic
- Logic Programming with Focusing Proofs in Linear Logic
- Logic programming in a fragment of intuitionistic linear logic
- Multimodal linguistic inference
- On Lambek's restriction in the presence of exponential modalities
- On the complexity of linear authorization logics
- On translating Lambek grammars with one division into context-free grammars
- Quantales and (noncommutative) linear logic
- Recursive unsolvability of a problem of Thue
- Relationships between nondeterministic and deterministic tape complexities
- Some Decision Problems in the Theory of Syntactic Categories
- Some Syntactical Observations on Linear Logic
- Subexponential concurrent constraint programming
- The Lambek calculus enriched with additional connectives
- The Mathematics of Sentence Structure
- The logic of categorial grammars. A deductive account of natural language syntax and semantics
- Undecidability of the Lambek calculus with a relevant modality
- Undecidability of the Lambek calculus with subexponential and bracket modalities
Cited in
(20)- A linear logic framework for multimodal logics
- A system of interaction and structure. IV: The exponentials and decomposition
- A fresh view of linear logic as a logical framework
- Soft subexponentials and multiplexing
- The multiplicative-additive Lambek calculus with subexponential and bracket modalities
- scientific article; zbMATH DE number 1418443 (Why is no real title available?)
- Universal proof theory: semi-analytic rules and Craig interpolation
- Versions of a local contraction subexponential in the Lambek calculus
- Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
- Relational Models for the Lambek Calculus with Intersection and Constants
- Kleene star, subexponentials without contraction, and infinite computations
- Non-associative, non-commutative multi-modal linear logic
- Explorations in Subexponential Non-associative Non-commutative Linear Logic
- Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Infinitary action logic with multiplexing
- Specifying proof systems in linear logic with subexponentials
- Complexity of Lambek calculi with modalities and of total derivability in grammars
- Infinitary action logic with exponentiation
- On noncommutative extensions of linear logic
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)
