Subexponentials in non-commutative linear logic
From MaRDI portal
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
- 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
- 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?)
- 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 in a fragment of intuitionistic linear logic
- Logic Programming with Focusing Proofs in 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 logic of categorial grammars. A deductive account of natural language syntax and semantics
- The Mathematics of Sentence Structure
- Undecidability of the Lambek calculus with a relevant modality
- Undecidability of the Lambek calculus with subexponential and bracket modalities
Cited in
(25)- The multiplicative-additive Lambek calculus with subexponential and bracket modalities
- Complexity of Lambek calculi with modalities and of total derivability in grammars
- Infinitary action logic with exponentiation
- Soft subexponentials and multiplexing
- Non-associative, non-commutative multi-modal linear logic
- Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
- A fresh view of linear logic as a logical framework
- Kleene star, subexponentials without contraction, and infinite computations
- Infinitary action logic with multiplexing
- A system of interaction and structure. IV: The exponentials and decomposition
- scientific article; zbMATH DE number 1418443 (Why is no real title available?)
- On noncommutative extensions of linear logic
- Specifying proof systems in linear logic with subexponentials
- A linear logic framework for multimodal logics
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Versions of a local contraction subexponential in the Lambek calculus
- Relational Models for the Lambek Calculus with Intersection and Constants
- Explorations in Subexponential Non-associative Non-commutative Linear Logic
- Semantic Analysis of Subexponential Modalities in Distributive Non-commutative Linear Logic
- Universal proof theory: semi-analytic rules and Craig interpolation
- On syntactic concept lattice models for the Lambek calculus and infinitary action logic
- Relational models for the Lambek calculus with local contraction subexponentials
- Lambek calculus with banged atoms for parasitic gaps
- YALLA: yet another deep embedding of linear logic in Rocq
- Universal proof theory: semi-analytic rules and uniform interpolation
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)
