{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T04:24:47Z","timestamp":1729743887389,"version":"3.28.0"},"reference-count":23,"publisher":"Oxford University Press (OUP)","issue":"7","license":[{"start":{"date-parts":[[2023,8,10]],"date-time":"2023-08-10T00:00:00Z","timestamp":1691625600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024,10,23]]},"abstract":"Abstract<\/jats:title>\n Sequent-style refutation calculi with non-invertible rules are challenging to design because multiple proof-search strategies need to be simultaneously verified. In this paper, we present a refutation calculus for the multiplicative\u2013additive fragment of linear logic ($\\textsf{MALL}$) whose binary rule for the multiplicative conjunction $(\\otimes )$ and the unary rule for the additive disjunction $(\\oplus )$ fail invertibility. Specifically, we design a cut-free hypersequent calculus $\\textsf{HMALL}$, which is equivalent to $\\textsf{MALL}$, and obtained by transforming the usual tree-like shape of derivations into a parallel and linear structure. Next, we develop a refutation calculus $\\overline{\\textsf{HMALL}}$ based on the calculus $\\textsf{HMALL}$. As far as we know, this is also the first refutation calculus for a substructural logic. Finally, we offer a fractional semantics for $\\textsf{MALL}$\u2014whereby its formulas are interpreted by a rational number in the closed interval [0, 1] \u2014thus extending to the substructural landscape the project of fractional semantics already pursued for classical and modal logics.<\/jats:p>","DOI":"10.1093\/logcom\/exad048","type":"journal-article","created":{"date-parts":[[2023,8,13]],"date-time":"2023-08-13T22:25:07Z","timestamp":1691965507000},"page":"1249-1273","source":"Crossref","is-referenced-by-count":0,"title":["Linear logic in a refutational setting"],"prefix":"10.1093","volume":"34","author":[{"given":"Mario","family":"Piazza","sequence":"first","affiliation":[{"name":"Scuola Normale Superiore di Pisa"}]},{"given":"Gabriele","family":"Pulcini","sequence":"additional","affiliation":[{"name":"Dipartimento di Studi letterari, filosofici e di Storia dell\u2019arte , Universit\u00e0 di Roma \u201cTor Vergata\u201d"}]},{"given":"Matteo","family":"Tesi","sequence":"additional","affiliation":[{"name":"Scuola Normale Superiore di Pisa"}]}],"member":"286","published-online":{"date-parts":[[2023,8,10]]},"reference":[{"key":"2024102321261983700_ref1","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"2024102321261983700_ref2","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":"2024102321261983700_ref3","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","author":"Avron","year":"1996"},{"key":"2024102321261983700_ref4","first-page":"273","article-title":"Cut-elimination and deductive polarization in complementary classical logic","volume":"25","author":"Carnielli","year":"2017","journal-title":"Logic Journal of the IGPL"},{"volume-title":"Computability An Introduction to Recursive Function Theory","year":"1980","author":"Cutland","key":"2024102321261983700_ref5"},{"key":"2024102321261983700_ref6","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1093\/jigpal\/jzn020","article-title":"Cut-based abduction","volume":"16","author":"D\u2019Agostino","year":"2008","journal-title":"Logic Journal of IGPL"},{"key":"2024102321261983700_ref7","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF01622878","article-title":"The structure of multiplicatives","volume":"28","author":"Danos","year":"1989","journal-title":"Archive for Mathematical Logic"},{"key":"2024102321261983700_ref8","first-page":"1","article-title":"Linear logic: its syntax and semantics","author":"Girard","year":"1995","journal-title":"London Mathematical Society Lecture Note Series"},{"key":"2024102321261983700_ref9","doi-asserted-by":"crossref","DOI":"10.4171\/088","volume-title":"The Blind Spot: Lectures on Logic","author":"Girard","year":"2011"},{"key":"2024102321261983700_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":"2024102321261983700_ref11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-981-15-2221-5_9","article-title":"Refutation systems: an overview and some applications to philosophical logics","volume-title":"Knowledge, Proof and Dynamics","author":"Goranko","year":"2020"},{"key":"2024102321261983700_ref12","doi-asserted-by":"crossref","first-page":"784","DOI":"10.1145\/1094622.1094629","article-title":"Proof nets for unit-free multiplicative-additive linear logic","volume":"6","author":"Hughes","year":"2005","journal-title":"ACM Transactions on Computational Logic"},{"key":"2024102321261983700_ref13","doi-asserted-by":"crossref","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","article-title":"Focusing and polarization in linear, intuitionistic, and classical logics","volume":"410","author":"Liang","year":"2009","journal-title":"Theoretical Computer Science"},{"key":"2024102321261983700_ref14","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1008399708659","article-title":"Linguistic applications of first order intuitionistic linear logic","volume":"10","author":"Moot","year":"2001","journal-title":"Journal of Logic, Language and Information"},{"key":"2024102321261983700_ref15","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-642-14287-1_11","article-title":"An analytic tableau system for natural logic","volume-title":"Logic, Language and Meaning","author":"Muskens","year":"2010"},{"key":"2024102321261983700_ref16","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1093\/logcom\/6.5.709","article-title":"Quantales and structural rules","volume":"6","author":"Piazza","year":"1996","journal-title":"Journal of Logic and Computation"},{"key":"2024102321261983700_ref17","doi-asserted-by":"crossref","first-page":"810","DOI":"10.1017\/S1755020319000431","article-title":"Fractional semantics for classical logic","volume":"13","author":"Piazza","year":"2020","journal-title":"The Review of Symbolic Logic"},{"key":"2024102321261983700_ref18","first-page":"1","article-title":"Fractional-valued modal logic","author":"Piazza","year":"2021","journal-title":"The Review of Symbolic Logic"},{"journal-title":"Forthcoming in the Bulletin of the Section of Logic","article-title":"Fractional-valued modal logic and soft bilateralism","author":"Piazza","key":"2024102321261983700_ref19"},{"key":"2024102321261983700_ref20","article-title":"Classical logic through rejection and refutation","volume-title":"Landscapes in Logic","author":"Pulcini","year":"2021"},{"key":"2024102321261983700_ref21","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-62688-3_43","article-title":"Pomset logic: a non-commutative extension of classical linear logic","volume-title":"International Conference on Typed Lambda Calculi and Applications","author":"Retor\u00e9","year":"1997"},{"key":"2024102321261983700_ref22","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-94-007-0479-4_2","article-title":"Refutation systems in propositional logic","volume-title":"Handbook of Philosophical Logic","author":"Skura","year":"2011"},{"key":"2024102321261983700_ref23","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/978-3-319-65430-0_40","article-title":"Rejection in Lukasiewicz\u2019s and S\u0142upecki\u2019s sense","volume-title":"The Lvov\u2013Warsaw School. Past and Present","author":"Wybraniec-Skardowska","year":"2018"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/7\/1249\/59997702\/exad048.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/34\/7\/1249\/59997702\/exad048.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T21:26:34Z","timestamp":1729718794000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/34\/7\/1249\/7240512"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,10]]},"references-count":23,"journal-issue":{"issue":"7","published-online":{"date-parts":[[2023,8,10]]},"published-print":{"date-parts":[[2024,10,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exad048","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2024,10]]},"published":{"date-parts":[[2023,8,10]]}}}