{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T00:18:29Z","timestamp":1722471509226},"reference-count":27,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we introduce a new logic that we call \u2018resource sharing linear logic (RSLL)\u2019. In linear logic (LL), formulas without modality express some resource-conscious situation (a formula can be used only once); formulas with modality express a situation with unlimited resources. We introduce the logic RSLL in which we have a strengthened modality (S5-modality) that can be understood as expressing not only unlimited resources but also resources shared by different agents. Observing that merely strengthening the modality allows weakening axiom to be derivable in a Hilbert-style formulation of this logic, we reformulate RSLL as a logic similar to affine logic by a hypersequent calculus that has weakening as a primitive rule. We prove the completeness of the hypersequent calculus with respect to phase semantics and the cut-elimination theorem for the system by a syntactical method. We also prove the decidability of RSLL via a computational interpretation of RSLL, which is a parallel version of Kopylov\u2019s computational model for LL. We then introduce an explicit counterpart of RSLL in the style of Artemov\u2019s justication logic (JRSLL). We prove a realization theorem for RSLL via its explicit counterpart.<\/jats:p>","DOI":"10.1093\/logcom\/exaa013","type":"journal-article","created":{"date-parts":[[2020,2,20]],"date-time":"2020-02-20T12:51:28Z","timestamp":1582203088000},"page":"295-319","source":"Crossref","is-referenced-by-count":0,"title":["Resource sharing linear logic"],"prefix":"10.1093","volume":"30","author":[{"given":"Hidenori","family":"Kurokawa","sequence":"first","affiliation":[{"name":"Institute of Liberal Arts and Sciences, Kanazawa University, Kakuma, Kanazawa 920-1192, Japan"}]},{"given":"Hirohiko","family":"Kushida","sequence":"first","affiliation":[{"name":"Computer Science Program, Graduate Center, City University of New York, 365 Fifth Avenue, New York, NY 10016, USA"}]}],"member":"286","published-online":{"date-parts":[[2020,3,3]]},"reference":[{"key":"2020040702352915900_ref1","article-title":"Justification logic","volume-title":"Stanford Encyclopedia of Philosophy","author":"Artemov","year":"2012"},{"key":"2020040702352915900_ref2","doi-asserted-by":"crossref","DOI":"10.1017\/9781108348034","article-title":"Cambridge Tracts in Mathematics","volume-title":"Justification Logic: Reasoning with Reasons","author":"Artemov","year":"2019"},{"key":"2020040702352915900_ref3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","article-title":"Explicit provability and constructive semantics","volume":"7","author":"Artemov","year":"2001","journal-title":"The Bulletin of Symbolic Logic"},{"key":"2020040702352915900_ref4","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(88)90037-0","article-title":"The semantics and proof theory of linear logic","volume":"57","author":"Avron","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"2020040702352915900_ref5","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","article-title":"Hypersequents, logical consequence, and intermediate logics for concurrency","volume":"4","author":"Avron","year":"1991","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2020040702352915900_ref6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/oso\/9780198538622.003.0001","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","volume-title":"Logic: From Foundations to Applications. Proc. Logic Colloquium","author":"Avron","year":"1996"},{"key":"2020040702352915900_ref7","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1305\/ndjfl\/1093635329","article-title":"Linear logic displayed","volume":"31","author":"Belnap","year":"1990","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2020040702352915900_ref8","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1007\/s00153-004-0265-8","article-title":"A proof-theoretical investigation of global intuitionistic (fuzzy) logic","volume":"44","author":"Ciabattoni","year":"2004","journal-title":"Archive for Mathematical Logic"},{"key":"2020040702352915900_ref9","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1016\/j.apal.2016.10.012","article-title":"Algebraic proof theory: hypersequents and hypercompletions","volume":"168","author":"Ciabattoni","year":"2017","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702352915900_ref10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2020040702352915900_ref11","first-page":"200","article-title":"Horn programming in linear logic is np-complete","volume-title":"Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS \u201992)","author":"Kanovich","year":"1992"},{"key":"2020040702352915900_ref12","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1109\/LICS.1995.523283","article-title":"Decidability of linear affine logic","volume-title":"Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science","author":"Kopylov","year":"1995"},{"key":"2020040702352915900_ref13","first-page":"51","article-title":"Hypersequent calculi for modal logics extending S4","volume-title":"New Frontiers in Artificial Intelligence\u2014JSAI-isAI 2013 Workshops, LENLS, JURISIN, MiMI, AAA, and DDS","author":"Kurokawa","year":"2013"},{"key":"2020040702352915900_ref14","first-page":"194","article-title":"Substructural logic of proofs","volume-title":"WoLLIC","author":"Kurokawa","year":"2013"},{"key":"2020040702352915900_ref15","doi-asserted-by":"crossref","first-page":"636","DOI":"10.1007\/s00224-009-9209-3","article-title":"Self-referential justifications in epistemic logic","volume":"46","author":"Kuznets","year":"2010","journal-title":"Theory of Computing Systems"},{"volume-title":"Logics of Proofs and Justifications","year":"2019","author":"Kuznets","key":"2020040702352915900_ref16"},{"key":"2020040702352915900_ref17","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1109\/LICS.2013.47","article-title":"From frame properties to hypersequent rules in modal logics","volume-title":"28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013","author":"Lahav","year":"2013"},{"key":"2020040702352915900_ref18","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1016\/j.fss.2009.09.001","article-title":"Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions","volume":"161","author":"Metcalfe","year":"2010","journal-title":"Fuzzy Sets and Systems"},{"key":"2020040702352915900_ref19","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/s11225-006-6608-1","article-title":"Cut elimination for S4C: a case study","volume":"82","author":"Mints","year":"2006","journal-title":"Studia Logica"},{"key":"2020040702352915900_ref20","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/S0304-3975(99)00058-4","article-title":"Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic","volume":"227","author":"Okada","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"2020040702352915900_ref21","first-page":"449","article-title":"Linear logic and intuitionistic logic","volume-title":"Revue Internationale de Philosophie","author":"Okada","year":"2004"},{"key":"2020040702352915900_ref22","first-page":"113","article-title":"Gentzen method in modal calculi I","author":"Onishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"2020040702352915900_ref23","first-page":"115","article-title":"Gentzen method in modal calculi II","author":"Onishi","year":"1959","journal-title":"Osaka Mathematical Journal"},{"key":"2020040702352915900_ref24","doi-asserted-by":"crossref","first-page":"687","DOI":"10.2977\/prims\/1195189604","article-title":"On some intuitionistic modal logics","volume":"13","author":"Ono","year":"1977","journal-title":"Publications of the Research Institute for Mathematical Sciences"},{"key":"2020040702352915900_ref25","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-3179-9","volume-title":"Substructural Logics: A Primer","author":"Paoli","year":"2002"},{"key":"2020040702352915900_ref26","first-page":"25","article-title":"Modalities in substructural logics","volume":"141\u2013142","author":"Restall","year":"1993","journal-title":"Logique et Analyse"},{"key":"2020040702352915900_ref27","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1093\/logcom\/exl030","article-title":"On realization of S5-modality by evidence terms","volume":"16","author":"Rubtsova","year":"2006","journal-title":"Journal of Logic and Computation"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/295\/33016405\/exaa013.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/295\/33016405\/exaa013.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T21:49:33Z","timestamp":1722462573000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/295\/5770983"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":27,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,3,3]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa013","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}