{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:02Z","timestamp":1767927842960,"version":"3.49.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319942049","type":"print"},{"value":"9783319942056","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_16","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T16:22:50Z","timestamp":1530289370000},"page":"228-245","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["A Logical Framework with Commutative and Non-commutative Subexponentials"],"prefix":"10.1007","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":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"16_CR1","first-page":"1","volume":"1","author":"K Ajdukiewicz","year":"1935","unstructured":"Ajdukiewicz, K.: Die syntaktische Konnexit\u00e4t. Studia Philosophica 1, 1\u201327 (1935)","journal-title":"Studia Philosophica"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J-M Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Logic Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Logic Comput."},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"47","DOI":"10.2307\/410452","volume":"29","author":"Y Bar-Hillel","year":"1953","unstructured":"Bar-Hillel, Y.: A quasi-arithmetical notation for syntactic description. Language 29, 47\u201358 (1953)","journal-title":"Language"},{"key":"16_CR4","volume-title":"Language in Action: Categories, Lambdas and Dynamic Logic","author":"J Benthem van","year":"1991","unstructured":"van Benthem, J.: Language in Action: Categories, Lambdas and Dynamic Logic. Elsevier, North Holland (1991)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: The structure of exponentials: uncovering the dynamics of linear logic proofs. In: G\u00f6del, K. (ed.) Colloquium, pp. 159\u2013171 (1993)","DOI":"10.1007\/BFb0022564"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR7","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS (1987)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic: extended abstract. In: LICS (1991)","DOI":"10.1109\/LICS.1991.151628"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-662-55751-8_26","volume-title":"Fundamentals of Computation Theory","author":"M Kanovich","year":"2017","unstructured":"Kanovich, M., Kuznetsov, S., Scedrov, A.: Undecidability of the Lambek calculus with subexponential and bracket modalities. In: Klasing, R., Zeitoun, M. (eds.) FCT 2017. LNCS, vol. 10472, pp. 326\u2013340. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-55751-8_26"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Kanovich, M., Kuznetsov, S., Nigam, V., Scedrov, A.: Subexponentials in non-commutative linear logic. Math. Struct. Comput. Sci., FirstView, 1\u201333 (2018). https:\/\/doi.org\/10.1017\/S0960129518000117","DOI":"10.1017\/S0960129518000117"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Kuznetsov, S., Morrill, G., Valent\u00edn, O.: Count-invariance including exponentials. In: Proceedings of MoL 2017, volume W17\u20133413 of ACL Anthology, pp. 128\u2013139 (2017)","DOI":"10.18653\/v1\/W17-3413"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1080\/00029890.1958.11989160","volume":"65","author":"J Lambek","year":"1958","unstructured":"Lambek, J.: The mathematics of sentence structure. Amer. Math. Mon. 65, 154\u2013170 (1958)","journal-title":"Amer. Math. Mon."},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D Miller","year":"1996","unstructured":"Miller, D.: Forum: a multiple-conclusion specification logic. Theor. Comput. Sci. 165(1), 201\u2013232 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Miller, D., Saurin, A.: From proofs to focused proofs: a modular proof of focalization in linear logic. In: CSL, pp. 405\u2013419 (2007)","DOI":"10.1007\/978-3-540-74915-8_31"},{"issue":"3\u20134","key":"16_CR15","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF00159344","volume":"5","author":"M Moortgat","year":"1996","unstructured":"Moortgat, M.: Multimodal linguistic inference. J. Logic Lang. Inf. 5(3\u20134), 349\u2013385 (1996)","journal-title":"J. Logic Lang. Inf."},{"key":"16_CR16","series-title":"Studies in Linguistics and Philosophy","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-50422-3_10","volume-title":"Modern Perspectives in Type-Theoretical Semantics","author":"R Moot","year":"2017","unstructured":"Moot, R.: The grail theorem prover: type theory for syntax and semantics. In: Chatzikyriakidis, S., Luo, Z. (eds.) Modern Perspectives in Type-Theoretical Semantics. SLP, vol. 98, pp. 247\u2013277. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-50422-3_10"},{"key":"16_CR17","unstructured":"Morrill, G.: CatLog: a categorial parser\/theorem-prover. In: LACL System demostration (2012)"},{"key":"16_CR18","unstructured":"Morrill, G.: Parsing logical grammar: CatLog3. In: Proceedings of LACompLing (2017)"},{"key":"16_CR19","unstructured":"Morrill, G., Valent\u00edn, O.: Computation coverage of TLG: nonlinearity. In: NLCS (2015)"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"29","DOI":"10.4204\/EPTCS.197.4","volume":"197","author":"Glyn Morrill","year":"2015","unstructured":"Morrill, G., Valent\u00edn, O.: Multiplicative-additive focusing for parsing as deduction. In: First International Workshop on Focusing (2015)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"16_CR21","unstructured":"Nigam, V.: Exploiting non-canonicity in the sequent calculus. Ph.D. thesis (2009)"},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.tcs.2014.02.018","volume":"536","author":"V Nigam","year":"2014","unstructured":"Nigam, V.: A framework for linear authorization logics. TCS 536, 21\u201341 (2014)","journal-title":"TCS"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Nigam, V., Miller, D.: Algorithmic specifications in linear logic with subexponentials. In: PPDP, pp. 129\u2013140 (2009)","DOI":"10.1145\/1599410.1599427"},{"issue":"2","key":"16_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10817-010-9182-1","volume":"45","author":"V Nigam","year":"2010","unstructured":"Nigam, V., Miller, D.: A framework for proof systems. J. Autom. Reasoning 45(2), 157\u2013188 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-40184-8_29","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"Vivek Nigam","year":"2013","unstructured":"Nigam, V., Olarte, C., Pimentel, E.: A general proof system for modalities in concurrent constraint programming. In: CONCUR (2013)"},{"issue":"2","key":"16_CR26","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1093\/logcom\/exu029","volume":"26","author":"V Nigam","year":"2016","unstructured":"Nigam, V., Pimentel, E., Reis, G.: An extended framework for specifying and reasoning about proof systems. J. Logic Comput. 26(2), 539\u2013576 (2016)","journal-title":"J. Logic Comput."},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1016\/j.tcs.2015.06.031","volume":"606","author":"C Olarte","year":"2015","unstructured":"Olarte, C., Pimentel, E., Nigam, V.: Subexponential concurrent constraint programming. Theor. Comput. Sci. 606, 98\u2013120 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Pentus, M.: Lambek grammars are context-free. In: LICS, pp. 429\u2013433 (1993)","DOI":"10.1109\/LICS.1993.287565"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Simmons, R.J.: Substructural operational semantics as ordered logic programming. In: LICS, pp. 101\u2013110 (2009)","DOI":"10.1109\/LICS.2009.8"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Polakow, J.: Linear logic programming with an ordered context. In: PPDP (2000)","DOI":"10.1145\/351268.351277"},{"key":"16_CR31","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00630917","volume":"8","author":"SM Shieber","year":"1985","unstructured":"Shieber, S.M.: Evidence against the context-freeness of natural languages. Linguist. Philos. 8, 333\u2013343 (1985)","journal-title":"Linguist. Philos."},{"key":"16_CR32","unstructured":"Simmons, R.J., Pfenning, F.: Weak focusing for ordered linear logic. Technical report CMU-CS-10-147 (2011)"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-24849-1_23","volume-title":"Types for Proofs and Programs","author":"K Watkins","year":"2004","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: the propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355\u2013377. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_23"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T12:51:33Z","timestamp":1751719893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}