{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T16:42:52Z","timestamp":1784306572661,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["22-01137S"],"award-info":[{"award-number":["22-01137S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200021_215157"],"award-info":[{"award-number":["200021_215157"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,10,31]]},"abstract":"<jats:p>We prove that there are continuum-many axiomatic extensions of the full Lambek calculus with exchange that have the deductive interpolation property. Further, we extend this result to both classical and intuitionistic linear logic as well as their multiplicative-additive fragments. None of the logics we exhibit have the Craig interpolation property, but we show that the exhibited extensions of classical and intuitionistic linear logic all enjoy a guarded form of Craig interpolation. We also give continuum-many axiomatic extensions of classical linear logic without the deductive interpolation property.<\/jats:p>","DOI":"10.1145\/3680284","type":"journal-article","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T15:56:04Z","timestamp":1721922964000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Interpolation in Linear Logic and Related Systems"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6025-8770","authenticated-orcid":false,"given":"Wesley","family":"Fussner","sequence":"first","affiliation":[{"name":"Institute of Computer Science, Czech Academy of Sciences, Prague, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9364-5149","authenticated-orcid":false,"given":"Simon","family":"Santschi","sequence":"additional","affiliation":[{"name":"Mathematical Institute, University of Bern, Bern, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,23]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"P. Aglian\u00f2. 2023. An algebraic investigation of linear logic. arXiv:2305.12408. Retrieved from https:\/\/arxiv.org\/abs\/2305.12408"},{"key":"e_1_3_2_3_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-030-88701-8_1","volume-title":"Proceedings of the 19th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921)","volume":"13027","author":"Aguzzoli S.","year":"2021","unstructured":"S. Aguzzoli and M. Bianchi. 2021. Amalgamation property for varieties of BL-algebras generated by one chain with finitely many components. In Proceedings of the 19th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921). U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter (Eds.), Lecture Notes in Computer Science, Vol. 13027, Springer, 1\u201318."},{"key":"e_1_3_2_4_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-031-28083-2_1","volume-title":"Proceedings of the 20th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921)","volume":"13896","author":"Aguzzoli S.","year":"2023","unstructured":"S. Aguzzoli and M. Bianchi. 2023. Amalgamation Property for Some Varieties of BL-Algebras Generated by One Finite Set of BL-Chains with Finitely Many Components. In Proceedings of the 20th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921). R. Gl\u00fcck, L. Santocanale, and M. Winter (Eds.), Lecture Notes in Computer Science, Vol. 13896. Springer, 1\u201316."},{"key":"e_1_3_2_5_2","volume-title":"Entailment","author":"Anderson A. R.","year":"1975","unstructured":"A. R. Anderson and N. D. Belnap. 1975. Entailment, Vol. 1. Princeton University Press."},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0304-3975(88)90037-0","article-title":"The semantics and proof theory of linear logic","volume":"57","author":"Avron A.","year":"1988","unstructured":"A. Avron. 1988. The semantics and proof theory of linear logic. Theoret. Comput. Sci. 57, 2\u20133 (1988), 161\u2013184.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_2_7_2","series-title":"Memoirs of the American Mathematical Society","volume-title":"Algebraizable Logics","author":"Blok W.J.","year":"1989","unstructured":"W.J. Blok and D. Pigozzi. 1989. Algebraizable Logics. In Memoirs of the American Mathematical Society, Vol. 77. American Mathematical Society."},{"key":"e_1_3_2_8_2","first-page":"75","volume-title":"Proceedings of the Algebraic Logic. Papers of a Colloquium","author":"Blok W.J.","year":"1991","unstructured":"W.J. Blok and D.L. Pigozzi. 1991. Local deduction theorems in algebraic logic. In Proceedings of the Algebraic Logic. Papers of a Colloquium J\u00e1nos Bolyai Mathematical Society, 75\u2013109."},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8130-3","volume-title":"A Course in Universal Algebra","author":"Burris S.","year":"1981","unstructured":"S. Burris and H. P. Sankappanavar. 1981. A Course in Universal Algebra. Springer Verlag, New York."},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1093\/logcom\/exn081","article-title":"Constructive logic with strong negation as a substructural logic","volume":"20","author":"Busaniche M.","year":"2010","unstructured":"M. Busaniche and R. Cignoli. 2010. Constructive logic with strong negation as a substructural logic. J. Logic Comput. 20 (2010), 761\u2013793.","journal-title":"J. Logic Comput."},{"key":"e_1_3_2_11_2","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/BF01190258","article-title":"Congruence distributive quasivarieties whose finitely subdirectly irreducible members form a universal class","volume":"27","author":"Czelakowski J.","year":"1990","unstructured":"J. Czelakowski and W. Dziobiak. 1990. Congruence distributive quasivarieties whose finitely subdirectly irreducible members form a universal class. Algebra Universalis 27 (1990), 128\u2013149.","journal-title":"Algebra Universalis"},{"key":"e_1_3_2_12_2","series-title":"Lecture Notes in Pure and Applied Mathematics","first-page":"187","volume-title":"Models, Algebras, and Proofs","author":"Czelakowski J.","year":"1999","unstructured":"J. Czelakowski and D. Pigozzi. 1999. Amalgamation and interpolation in abstract algebraic logic. In Models, Algebras, and Proofs. X. Caicedo and C. H. Montenegro (Eds.), Lecture Notes in Pure and Applied Mathematics, Vol. 203. Marcel Dekker, Inc., 187\u2013265."},{"issue":"2","key":"e_1_3_2_13_2","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1006\/jabr.1999.8136","article-title":"One chain generated varieties of MV-algebras","volume":"225","author":"Di Nola A.","year":"2000","unstructured":"A. Di Nola and A. Lettieri. 2000. One chain generated varieties of MV-algebras. J. Algebra 225, 2 (2000), 667\u2013697.","journal-title":"J. Algebra"},{"issue":"2","key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF01899665","article-title":"\u00dcber injektive Moduln","volume":"4","author":"Eckmann B.","year":"1953","unstructured":"B. Eckmann and A. Schopf. 1953. \u00dcber injektive Moduln. Archiv der Mathematik 4, 2 (1953), 75\u201378.","journal-title":"Archiv der Mathematik"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1006\/inco.2000.3002","article-title":"Linear concurrent constraint programming: Operational and phase semantics","volume":"165","author":"Fages F.","year":"2001","unstructured":"F. Fages, P. Ruet, and S. Soliman. 2001. Linear concurrent constraint programming: Operational and phase semantics. Inf. Comput. 165 (2001), 14\u201341.","journal-title":"Inf. Comput."},{"key":"e_1_3_2_16_2","volume-title":"Abstract Algebraic Logic: An Introductory Textbook","author":"Font J.","year":"2016","unstructured":"J. Font. 2016. Abstract Algebraic Logic: An Introductory Textbook. College Publications."},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11225-021-09956-z","article-title":"Poset products as relational models","volume":"110","author":"Fussner W.","year":"2022","unstructured":"W. Fussner. 2022. Poset products as relational models. Studia Logica 110 (2022), 95\u2013120.","journal-title":"Studia Logica"},{"key":"e_1_3_2_18_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/978-3-030-88701-8_11","volume-title":"Proceedings of the19th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921)","volume":"13027","author":"Fussner W.","year":"2021","unstructured":"W. Fussner and W. Zuluaga Botero. 2021. Some modal and temporal translations of generalized basic logic. In Proceedings of the19th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS \u201921). U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter (Eds.), Lecture Notes in Computer Science, Vol. 13027. Springer, 176\u2013191."},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"1188","DOI":"10.1016\/j.apal.2019.05.003","article-title":"Categories of models of R-mingle","volume":"170","author":"Fussner W.","year":"2019","unstructured":"W. Fussner and N. Galatos. 2019. Categories of models of R-mingle. Ann. Pure Appl. Logic 170 (2019), 1188\u20131242.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"7","key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"103443","DOI":"10.1016\/j.apal.2024.103443","article-title":"Semiconic idempotent logic I: Structure and local deduction theorems","volume":"175","author":"Fussner W.","year":"2024","unstructured":"W. Fussner and N. Galatos. 2024a. Semiconic idempotent logic I: Structure and local deduction theorems. Ann. Pure Appl. Logic 175, 7 (2024), 103443.","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"W. Fussner and N. Galatos. 2024b. Semiconic idempotent logic II: Beth definability and deductive interpolation. arXiv:2208.09724. Retrieved from https:\/\/arxiv.org\/abs\/2208.09724v3","DOI":"10.1016\/j.apal.2024.103528"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jalgebra.2023.11.003","article-title":"Transfer theorems for finitely subdirectly irreducible algebras","volume":"640","author":"Fussner W.","year":"2024","unstructured":"W. Fussner and G. Metcalfe. 2024. Transfer theorems for finitely subdirectly irreducible algebras. J. Algebra 640 (2024), 1\u201320.","journal-title":"J. Algebra"},{"key":"e_1_3_2_23_2","unstructured":"W. Fussner G. Metcalfe and S. Santschi. 2024. Interpolation and the exchange rule. arXiv:2310.14953. Retrieved from https:\/\/arxiv.org\/abs\/2310.14953"},{"key":"e_1_3_2_24_2","unstructured":"W. Fussner and S. Santschi. 2024. Interpolation in H\u00e1jek\u2019s basic logic.. arXiv:2403.13617. Retrieved from https:\/\/arxiv.org\/abs\/2403.13617"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-019-0612-6"},{"key":"e_1_3_2_26_2","volume-title":"Varieties of Residuated Lattices","author":"Galatos N.","year":"2003","unstructured":"N. Galatos. 2003. Varieties of Residuated Lattices. Ph.D. Dissertation. Vanderbilt University, Nashville."},{"key":"e_1_3_2_27_2","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"Galatos N.","year":"2007","unstructured":"N. Galatos, P. Jipsen, T. Kowalski, and H. Ono. 2007. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Elsevier."},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11225-006-8305-5","article-title":"Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL","volume":"83","author":"Galatos N.","year":"2006","unstructured":"N. Galatos and H. Ono. 2006. Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL. Studia Logica 83, 1\u20133 (2006), 279\u2013308.","journal-title":"Studia Logica"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard J.-Y.","year":"1987","unstructured":"J.-Y. Girard. 1987. Linear logic. Theoret. Comput. Sci. 50 (1987), 1\u2013101.","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"e_1_3_2_30_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3570919","article-title":"Linear logic properly displayed","volume":"24","author":"Grecco G.","year":"2023","unstructured":"G. Grecco and A. Palmigiano. 2023. Linear logic properly displayed. ACM Trans. Comput. Log. 24, 2 (2023), 1\u201356.","journal-title":"ACM Trans. Comput. Log."},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5300-3","volume-title":"Metamathematics of Fuzzy Logic","author":"H\u00e1jek P.","year":"1998","unstructured":"P. H\u00e1jek. 1998. Metamathematics of Fuzzy Logic. Kluwer."},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1086\/392742","article-title":"Interpolation as explanation","volume":"66","author":"Hintikka J.","year":"1999","unstructured":"J. Hintikka and I. Halonen. 1999. Interpolation as explanation. Philos. Sci. 66 (1999), 423.","journal-title":"Philos. Sci."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"90","DOI":"10.2178\/jsl\/1208358744","article-title":"Flat algebras and the translation of universal horn logic to equational logic","volume":"73","author":"Jackson M.","year":"2008","unstructured":"M. Jackson. 2008. Flat algebras and the translation of universal horn logic to equational logic. J. Symbolic Logic 73 (2008), 90\u2013128.","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1093\/logcom\/exn084","article-title":"Interpolation properties, Beth definability properties and amalgamation properties for substructural logics","volume":"20","author":"Kihara H.","year":"2010","unstructured":"H. Kihara and H. Ono. 2010. Interpolation properties, Beth definability properties and amalgamation properties for substructural logics. J. Logic Comput. 20, 4 (2010), 823\u2013875.","journal-title":"J. Logic Comput."},{"key":"e_1_3_2_35_2","first-page":"79","article-title":"Categorical algebraic properties. A compendium of amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity","volume":"18","author":"Kiss E.W.","year":"1983","unstructured":"E.W. Kiss, L. M\u00e1rki, P. Pr\u00f6hle, and W. Tholen. 1983. Categorical algebraic properties. A compendium of amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Stud. Sci. Math. Hung. 18 (1983), 79\u2013141.","journal-title":"Stud. Sci. Math. Hung."},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/BF01670006","article-title":"Craig\u2019s theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras","volume":"16","author":"Maksimova L.L.","year":"1977","unstructured":"L.L. Maksimova. 1977. Craig\u2019s theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras. Algebra Logika 16 (1977), 643\u2013681.","journal-title":"Algebra Logika"},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","article-title":"Forum: A multiple-conclusion specification logic","volume":"165","author":"Miller D.","year":"1996","unstructured":"D. Miller. 1996. Forum: A multiple-conclusion specification logic. Theoret. Comput. Sci. 165 (1996), 201\u2013232.","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_3_2_38_2","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1016\/j.apal.2005.11.001","article-title":"Interpolation and Beth\u2019s property in many-valued logic: A semantic investigation","volume":"141","author":"Montagna F.","year":"2006","unstructured":"F. Montagna. 2006. Interpolation and Beth\u2019s property in many-valued logic: A semantic investigation. Ann. Pure Appl. Logic 141 (2006), 148\u2013179.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"2","key":"e_1_3_2_39_2","first-page":"790","article-title":"The finite model property for various fragments of intuitionistic linear logic","volume":"64","author":"Okada M.","year":"1999","unstructured":"M. Okada and K. Terui. 1999. The finite model property for various fragments of intuitionistic linear logic. J. Logic 64, 2 (1999), 790\u2013802.","journal-title":"J. Logic"},{"issue":"2","key":"e_1_3_2_40_2","doi-asserted-by":"crossref","first-page":"419","DOI":"10.2307\/2275398","article-title":"Interpolation in fragments of classical linear logic","volume":"59","author":"Roorda D.","year":"1994","unstructured":"D. Roorda. 1994. Interpolation in fragments of classical linear logic. J. Symbolic Logic 59, 2 (1994), 419\u2013444.","journal-title":"J. Symbolic Logic"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s11225-008-9113-x","article-title":"Constructive logic with strong negation is a substructural logic I","volume":"88","author":"Spinks M.","year":"2008","unstructured":"M. Spinks and R. Veroff. 2008. Constructive logic with strong negation is a substructural logic I. Studia Logica 88 (2008), 325\u2013348.","journal-title":"Studia Logica"},{"key":"e_1_3_2_42_2","series-title":"CSLI Lecture Notes","volume-title":"Lectures on Linear Logic","author":"Troelstra A. S.","year":"1992","unstructured":"A. S. Troelstra. 1992. Lectures on Linear Logic. In CSLI Lecture Notes, Vol. 29. Center for the Study of Language and Information."},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01879739","article-title":"On McKenzie\u2019s method","volume":"32","author":"Willard R.","year":"1996","unstructured":"R. Willard. 1996. On McKenzie\u2019s method. Period. Math. Hung. 32 (1996), 149\u2013165.","journal-title":"Period. Math. Hung."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3680284","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3680284","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:21Z","timestamp":1750298241000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3680284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,23]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,10,31]]}},"alternative-id":["10.1145\/3680284"],"URL":"https:\/\/doi.org\/10.1145\/3680284","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,23]]},"assertion":[{"value":"2023-08-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-14","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}