Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, pp. 228–245
2018 · DOI: 10.1007/978-3-319-94205-6\_16
Logical frameworks allow the specification of deductive systems usingthe same logical machinery. Linear logical frameworks have been successfullyused for the specification of a number of computational, logics and proofsystems. Its success relies on the fact that formulas can be distinguished as linear,which behave intuitively as resources, and unbounded, which behave intuitionistically.Commutative subexponentials enhance the expressiveness of linear logicframeworks by allowing the distinction of multiple contexts. These contexts maybehave as multisets of formulas or sets of formulas. Motivated by applicationsin distributed systems and in type-logical grammar, we propose a linear logicalframework containing both commutative and non-commutative subexponentials.Non-commutative subexponentials can be used to specify contexts which behaveas lists, not multisets, of formulas. In addition, motivated by our applications intype-logical grammar, where the weakenening rule is disallowed, we investigatethe proof theory of formulas that can only contract, but not weaken. In fact, ourcontraction is non-local. We demonstrate that under some conditions such formulasmay be treated as unbounded formulas, which behave intuitionistically.