{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T22:30:24Z","timestamp":1768343424135,"version":"3.49.0"},"reference-count":59,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2018,5,2]],"date-time":"2018-05-02T00:00:00Z","timestamp":1525219200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:p>Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation 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 organised as sets and multisets of formulae not being possible to organise 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 the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.<\/jats:p>","DOI":"10.1017\/s0960129518000117","type":"journal-article","created":{"date-parts":[[2018,5,2]],"date-time":"2018-05-02T09:37:23Z","timestamp":1525253843000},"page":"1217-1249","source":"Crossref","is-referenced-by-count":26,"title":["Subexponentials in non-commutative linear logic"],"prefix":"10.1017","volume":"29","author":[{"given":"MAX","family":"KANOVICH","sequence":"first","affiliation":[]},{"given":"STEPAN","family":"KUZNETSOV","sequence":"additional","affiliation":[]},{"given":"VIVEK","family":"NIGAM","sequence":"additional","affiliation":[]},{"given":"ANDRE","family":"SCEDROV","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2018,5,2]]},"reference":[{"key":"S0960129518000117_ref58","first-page":"1","article-title":"Probleme \u00fcber Ver\u00e4nderungen von Zeichenreihen nach gegebener Regeln","volume":"10","author":"Thue","year":"1914","journal-title":"Christiana Videnskabs-Selskabets Skrifter"},{"key":"S0960129518000117_ref56","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.537"},{"key":"S0960129518000117_ref22","unstructured":"Kanovich M. , Kuznetsov S. and Scedrov A. (2016c). On Lambek's restriction in the presence of exponential modalities. In: Artemov S. and Nerode A. (eds.) Proceedings of the International Symposium on Logical Foundations of Computer Science (LFCS '16), Lecture Notes in Computer Science, vol. 9537, Springer, 146\u2013158."},{"key":"S0960129518000117_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/BF00630917"},{"key":"S0960129518000117_ref49","doi-asserted-by":"publisher","DOI":"10.2307\/2369451"},{"key":"S0960129518000117_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00045-X"},{"key":"S0960129518000117_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"S0960129518000117_ref29","unstructured":"Lambek J. (1969). Deductive systems and categories II. Standard constructions and closed categories. In: Category Theory, Homology Theory and Their Applications I, Lecture Notes in Mathematics, vol. 86, Springer, 76\u2013122."},{"key":"S0960129518000117_ref14","unstructured":"Hodas J. and Miller D. (1991). Logic programming in a fragment of intuitionistic linear logic. Extended abstract. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS '91) 32\u201342."},{"key":"S0960129518000117_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022564"},{"key":"S0960129518000117_ref8","first-page":"15","article-title":"Lambek calculus and substructural logics","volume":"36","author":"Buszkowski","year":"2010","journal-title":"Linguistic Analysis"},{"key":"S0960129518000117_ref17","unstructured":"Kanazawa M. (1999). Lambek calculus: Recognizing power and complexity. In: Johannes Franciscus Abraham Karel (JFAK). Essays dedicated to Johan van Benthem to the occasion of his 50th birthday. Vossiuspers, Amsterdam Univ. Press."},{"key":"S0960129518000117_ref6","doi-asserted-by":"crossref","unstructured":"Bra\u00fcner T. and de Paiva V. (1998). A formulation of linear logic based on dependency relations. In: Proceedings of the International Workshop on Computer Science Logic (CSL '97), Lecture Notes in Computer Science, vol. 1414, Springer, 129\u2013148.","DOI":"10.1007\/BFb0028011"},{"key":"S0960129518000117_ref5","volume-title":"Language in Action: Categories, Lambdas and Dynamic Logic","author":"Benthem","year":"1991"},{"key":"S0960129518000117_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129518000117_ref50","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287565"},{"key":"S0960129518000117_ref18","volume-title":"Extended abstract, presented at the 8th Annual Conference of the European Association for Computer Science Logic (CSL '94)","author":"Kanovich","year":"1994"},{"key":"S0960129518000117_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0960129518000117_ref41","first-page":"51","volume-title":"Proceedings of the Natural Language and Computer Science (NLCS '15)","author":"Morrill","year":"2015"},{"key":"S0960129518000117_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-55751-8_26"},{"key":"S0960129518000117_ref39","unstructured":"Morrill G. (2017a). Parsing logical grammar: CatLog3. In: Proceedings of the Workshop on Logic and Algorithms in Computational Linguistics (LACompLing '17), Stockholm University, 107\u2013131."},{"key":"S0960129518000117_ref9","doi-asserted-by":"crossref","unstructured":"Chaudhuri K. (2010). Classical and intuitionistic subexponential logics are equally expressive. In: Proceedings of the International Workshop on Computer Science Logic (CSL '10), Lecture Notes in Computer Science, vol. 6247, Springer, 185\u2013199.","DOI":"10.1007\/978-3-642-15205-4_17"},{"key":"S0960129518000117_ref7","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19820283308"},{"key":"S0960129518000117_ref43","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.61"},{"key":"S0960129518000117_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/BF00159344"},{"key":"S0960129518000117_ref3","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"S0960129518000117_ref32","first-page":"583","article-title":"On the impossibility of certain algorithms in the theory of associative systems","volume":"55","author":"Markov","year":"1947","journal-title":"Doklady Academy of Sciences USSR (N. S.)"},{"key":"S0960129518000117_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BF00171695"},{"key":"S0960129518000117_ref33","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316062"},{"key":"S0960129518000117_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.06.031"},{"key":"S0960129518000117_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s10988-016-9197-0"},{"key":"S0960129518000117_ref13","first-page":"95","volume-title":"Language and Grammar","author":"de Groote","year":"2005"},{"key":"S0960129518000117_ref15","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"S0960129518000117_ref45","unstructured":"Nigam V. and Miller D. (2009). Algorithmic specifications in linear logic with subexponentials. In: Proceedings of the Principles and Practice of Declarative Programming (PPDP '09) 129\u2013140."},{"key":"S0960129518000117_ref19","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523282"},{"key":"S0960129518000117_ref26","doi-asserted-by":"publisher","DOI":"10.1134\/S0081543816060080"},{"key":"S0960129518000117_ref30","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1093\/oso\/9780198537779.003.0008","volume-title":"Substructural Logics","author":"Lambek","year":"1993"},{"key":"S0960129518000117_ref20","unstructured":"Kanovich M. , Kuznetsov S. and Scedrov A. (2016a). Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities. arXiv 1608.02254."},{"key":"S0960129518000117_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-22110-5_7"},{"key":"S0960129518000117_ref21","unstructured":"Kanovich M. , Kuznetsov S. and Scedrov A. (2016b). Undecidability of the Lambek calculus with a relevant modality. In: Proceedings of the International Conference on Formal Grammar (FG '15 and '16), Lecture Notes in Computer Science, vol. 9804, Springer, 240\u2013256."},{"key":"S0960129518000117_ref2","first-page":"1","article-title":"Die syntaktische Konnexit\u00e4t","volume":"1","author":"Ajdukiewicz","year":"1935","journal-title":"Studia Philosophica"},{"key":"S0960129518000117_ref24","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/W17-3414"},{"key":"S0960129518000117_ref25","doi-asserted-by":"publisher","DOI":"10.3103\/S0027132211040085"},{"key":"S0960129518000117_ref27","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1958.11989160"},{"key":"S0960129518000117_ref53","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.8"},{"key":"S0960129518000117_ref28","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/012\/9972"},{"key":"S0960129518000117_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31555-8"},{"key":"S0960129518000117_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.018"},{"key":"S0960129518000117_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.018"},{"key":"S0960129518000117_ref59","doi-asserted-by":"publisher","DOI":"10.2307\/2274953"},{"key":"S0960129518000117_ref46","doi-asserted-by":"crossref","unstructured":"Nigam V. , Olarte C. and Pimentel E. (2013). A general proof system for modalities in concurrent constraint programming. In: Proceedings of the International Conference on Concurrency Theory (CONCUR '13), Lecture Notes in Computer Science, vol. 8052, Springer, 410\u2013424.","DOI":"10.1007\/978-3-642-40184-8_29"},{"key":"S0960129518000117_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50422-3_10"},{"key":"S0960129518000117_ref4","doi-asserted-by":"publisher","DOI":"10.2307\/410452"},{"key":"S0960129518000117_ref47","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu029"},{"key":"S0960129518000117_ref54","doi-asserted-by":"publisher","DOI":"10.2307\/2267170"},{"key":"S0960129518000117_ref55","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"S0960129518000117_ref36","volume-title":"Handbook of Logic and Language","author":"Moortgat","year":"1997"},{"key":"S0960129518000117_ref1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360103"},{"key":"S0960129518000117_ref42","volume-title":"Categorial Grammar: Logical Syntax, Semantics, and Processing","author":"Morrill","year":"2011"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,6]],"date-time":"2024-07-06T12:29:36Z","timestamp":1720268976000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000117\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,2]]},"references-count":59,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["S0960129518000117"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000117","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,2]]}}}