{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T03:33:24Z","timestamp":1763436804477,"version":"3.41.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,1,17]],"date-time":"2024-01-17T00:00:00Z","timestamp":1705449600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Marie Sk\u0142odowska-Curie","award":["101007627"],"award-info":[{"award-number":["101007627"]}]},{"name":"Chinese Ministry of Education of Humanities and Social Science Project","award":["23YJC72040003"],"award-info":[{"award-number":["23YJC72040003"]}]},{"name":"Young Scholars Program of Shandong University","award":["11090089964225"],"award-info":[{"award-number":["11090089964225"]}]},{"name":"NWO","award":["KIVI.2019.001"],"award-info":[{"award-number":["KIVI.2019.001"]}]},{"name":"Key Project of Chinese Ministry of Education","award":["22JJD720021"],"award-info":[{"award-number":["22JJD720021"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,1,31]]},"abstract":"<jats:p>\n            In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the\n            <jats:italic>residuated frames<\/jats:italic>\n            in \u00a0Reference [\n            <jats:xref ref-type=\"bibr\">34<\/jats:xref>\n            ] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathrm{D.LE}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            associated with the basic normal LE-logics and their axiomatic extensions with analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus\n            <jats:inline-formula content-type=\"math\/tex\">\n              <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\mathrm{D.LE}\\)<\/jats:tex-math>\n            <\/jats:inline-formula>\n            , as well as for its extensions with analytic structural rules satisfying certain additional properties.\n          <\/jats:p>","DOI":"10.1145\/3632526","type":"journal-article","created":{"date-parts":[[2023,11,17]],"date-time":"2023-11-17T12:12:29Z","timestamp":1700223149000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Algebraic Proof Theory for LE-logics"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4845-3821","authenticated-orcid":false,"given":"Giuseppe","family":"Greco","sequence":"first","affiliation":[{"name":"School of Business and Economics, Vrije Universiteit Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8608-808X","authenticated-orcid":false,"given":"Peter","family":"Jipsen","sequence":"additional","affiliation":[{"name":"Faculty of Mathematics, Chapman University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-3197-1565","authenticated-orcid":false,"given":"Fei","family":"Liang","sequence":"additional","affiliation":[{"name":"School of Philosophy and Social Development, Shandong University, China and Institute of Logic and Cognition, Sun Yat-Sen University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9656-7527","authenticated-orcid":false,"given":"Alessandra","family":"Palmigiano","sequence":"additional","affiliation":[{"name":"School of Business and Economics, Vrije Universiteit Amsterdam, The Netherlands and Department of Mathematics and Applied Mathematics, University of Johannesburg, South Africa"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6228-4198","authenticated-orcid":false,"given":"Apostolos","family":"Tzimoulis","sequence":"additional","affiliation":[{"name":"School of Business and Economics, Vrije Universiteit Amsterdam, The Netherlands and Institute of Logic and Cognition, Sun Yat-Sen University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,17]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1023\/B:STUD.0000037127.15182.2a"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00284976"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S175502031700034X"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/s000120200000"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-04-03654-2"},{"key":"e_1_3_3_7_2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/978-3-642-01748-3_4","volume-title":"Languages: From Formal to Natural","author":"Buszkowski Wojciech","year":"2009","unstructured":"Wojciech Buszkowski and Maciej Farulewski. 2009. Nonassociative Lambek calculus with additives and context-free languages. In Languages: From Formal to Natural. Springer, 45\u201358."},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104756"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3529255","article-title":"Syntactic completeness of proper display calculi","volume":"23","author":"Chen Jinsheng","year":"2022","unstructured":"Jinsheng Chen, Giuseppe Greco, Alessandra Palmigiano, and Apostolos Tzimoulis. 2022. Syntactic completeness of proper display calculi. ACM Trans. Computat. Logic 23, 4 (2022), 1\u201346.","journal-title":"ACM Trans. Computat. Logic"},{"key":"e_1_3_3_10_2","first-page":"229","volume-title":"23rd Annual IEEE Symposium on Logic in Computer Science","author":"Ciabattoni Agata","year":"2008","unstructured":"Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. 2008. From axioms to analytic rules in nonclassical logics. In 23rd Annual IEEE Symposium on Logic in Computer Science. IEEE, 229\u2013240."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.003"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2874775"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-6607-2"},{"key":"e_1_3_3_14_2","first-page":"721","article-title":"Modelling competing theories","volume":"1905","author":"Conradie Willem","year":"2019","unstructured":"Willem Conradie, Andrew Craig, Alessandra Palmigiano, and Nachoem M. Wijnberg. 2019. Modelling competing theories. Conference of the European Society for Fuzzy Logic and Technology. ArXiv preprint 1905.11748. 721\u2013739.","journal-title":"Conference of the European Society for Fuzzy Logic and Technology."},{"key":"e_1_3_3_15_2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-662-59533-6_9","volume-title":"Logic, Language, Information, and Computation","author":"Conradie Willem","year":"2019","unstructured":"Willem Conradie, Andrew Craig, Alessandra Palmigiano, and Nachoem M. Wijnberg. 2019. Modelling informational entropy. In Logic, Language, Information, and Computation(LNCS, Vol. 11541), R. Iemhoff, M. Moortgat, and R. de Queiroz (Eds.). Springer, 140\u2013160."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2020.05.074"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.251.12"},{"key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-662-52921-8_10","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Conradie Willem","year":"2016","unstructured":"Willem Conradie, Sabine Frittella, Alessandra Palmigiano, Michele Piazzai, Apostolos Tzimoulis, and Nachoem M. Wijnberg. 2016. Categories: How I learned to stop worrying and love two sorts. In International Workshop on Logic, Language, Information, and Computation. Springer, 145\u2013164."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06025-5_36"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.10.004"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2019.04.003"},{"issue":"3","key":"e_1_3_3_22_2","first-page":"1","article-title":"Constructive canonicity of inductive inequalities","volume":"16","author":"Conradie Willem","year":"2020","unstructured":"Willem Conradie and Alessandra Palmigiano. 2020. Constructive canonicity of inductive inequalities. Logic. Meth. Comput. Sci. 16, 3 (2020), 1\u201339.","journal-title":"Logic. Meth. Comput. Sci."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2020.02.005"},{"key":"e_1_3_3_24_2","unstructured":"Willem Conradie Alessandra Palmigiano Claudette Robinson Apostolos Tzimoulis and Nachoem M. Wijnberg. 2019. The logic of vague categories. ArXiv:1908.04816."},{"key":"e_1_3_3_25_2","series-title":"(Landscapes in Logic","first-page":"38","volume-title":"Contemporary Logic and Computing","author":"Conradie Willem","year":"2020","unstructured":"Willem Conradie, Alessandra Palmigiano, Claudette Robinson, and Nachoem Wijnberg. 2020. Non-distributive logics: From semantics to meaning. In Contemporary Logic and Computing, Adrian Rezus (Ed.). (Landscapes in Logic, Vol. 1). College Publications, 38\u201386."},{"key":"e_1_3_3_26_2","unstructured":"Willem Conradie Alessandra Palmigiano and Apostolos Tzimoulis. [n. d.]. Goldblatt-Thomason for LE-logics. ([n. d.]). ArXiv:1809.08225."},{"key":"e_1_3_3_27_2","volume-title":"Introduction to Lattices and Order","author":"Davey Brian A.","year":"2022","unstructured":"Brian A. Davey and Hilary A. Priestley. 2022. Introduction to Lattices and Order. Cambridge University Press."},{"key":"e_1_3_3_28_2","volume-title":"European Workshop on Logics in AI (JELIA\u201990)","author":"Dunn J. Michael","year":"1990","unstructured":"J. Michael Dunn. 1990. Gaggle theory: An abstraction of Galois connections and residuation with application to negation and various logical operations. In European Workshop on Logics in AI (JELIA\u201990). Berlin Springer."},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537779.003.0004"},{"issue":"516","key":"e_1_3_3_30_2","article-title":"In so many possible worlds","volume":"4","author":"Fine Kit","year":"1972","unstructured":"Kit Fine. 1972. In so many possible worlds. Notre Dame J. Form. Logic 4 (1972), 516\u2013520.","journal-title":"Notre Dame J. Form. Logic"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu064"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu068"},{"key":"e_1_3_3_33_2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-662-52921-8_14","volume-title":"23rd International Workshop on Logic, Language, Information, and Computation (WoLLIC\u201916)","author":"Frittella Sabine","year":"2016","unstructured":"Sabine Frittella, Giuseppe Greco, Alessandra Palmigiano, and Fan Yang. 2016. A multi-type calculus for inquisitive logic. In 23rd International Workshop on Logic, Language, Information, and Computation (WoLLIC\u201916), R. de Queiroz J. V\u00e4\u00e4n\u00e4nen, \u00c5. Hirvonen (Ed.). Springer, 215\u2013233."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.05.004"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-2012-05573-5"},{"key":"e_1_3_3_36_2","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","author":"Galatos Nikolaos","year":"2007","unstructured":"Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. 2007. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Vol. 151. Elsevier."},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-006-8305-5"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.01.003"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1006\/jabr.2000.8622"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.007"},{"issue":"51","key":"e_1_3_3_41_2","first-page":"323","article-title":"Grades of modalities","volume":"13","author":"Goble Lou F.","year":"1970","unstructured":"Lou F. Goble. 1970. Grades of modalities. Logiq. Analy. 13, 51 (1970), 323\u2013334.","journal-title":"Logiq. Analy."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00652069"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.669"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.3.451"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58771-3_14"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.07.007"},{"issue":"5","key":"e_1_3_3_47_2","first-page":"853","article-title":"Vector spaces as Kripke frames","volume":"7","author":"Greco Giuseppe","year":"2020","unstructured":"Giuseppe Greco, Fei Liang, Michael Moortgat, and Alessandra Palmigiano. 2020. Vector spaces as Kripke frames. J. Appl. Logic \u2013 IfCoLog J. Logics Their Applic. 7, 5 (2020), 853\u2013873. https:\/\/arxiv.org\/abs\/1908.05528","journal-title":"J. Appl. Logic \u2013 IfCoLog J. Logics Their Applic."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-55386-2_14"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2018.05.007"},{"issue":"7","key":"e_1_3_3_50_2","first-page":"1367","article-title":"Unified correspondence as a proof-theoretic tool","volume":"28","author":"Greco Giuseppe","year":"2018","unstructured":"Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Apostolos Tzimoulis, and Zhiguang Zhao. 2018. Unified correspondence as a proof-theoretic tool. J. Logic Computat. 28, 7 (2018), 1367\u20131442.","journal-title":"J. Logic Computat."},{"key":"e_1_3_3_51_2","unstructured":"Vyacheslav N. Grishin. 1983. On a generalization of the Ajdukiewicz-Lambek system. In Studies in Nonclassical Logics and Formal Systems A. Mikhailov (Ed.). 315\u2013334."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.004"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.2307\/2372123"},{"key":"e_1_3_3_54_2","unstructured":"Hitoshi Kihara and Hiroakira Ono. 2008. Algebraic characterizations of variable separation properties. Rep. Math. Logic 43 (2008) 43\u201363."},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn084"},{"key":"e_1_3_3_56_2","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-94-017-2798-3_7","volume-title":"Proof Theory of Modal Logic","author":"Kracht Marcus","year":"1996","unstructured":"Marcus Kracht. 1996. Power and weakness of the modal display calculus. In Proof Theory of Modal Logic(Applied Logic Series, Vol. 2). Kluwer, 93\u2013121."},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.1134\/S0081543812070036"},{"key":"e_1_3_3_58_2","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/978-3-540-73445-1_19","volume-title":"International Workshop on Logic, Language, Information, and Computation","author":"Moortgat Michael","year":"2007","unstructured":"Michael Moortgat. 2007. Symmetries in natural language syntax and semantics: The Lambek-Grishin calculus. In International Workshop on Logic, Language, Information, and Computation. Springer, 264\u2013284."},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.2969\/msjmemoirs\/00201C060"},{"key":"e_1_3_3_60_2","first-page":"643","volume-title":"14th Conference Advances in Modal Logic (AiML\u201922)","volume":"14","author":"Panettiere Mattia","unstructured":"Mattia Panettiere and Apostolos Tzimoulis. [n. d.]. Graded modal logic with a single modality. In 14th Conference Advances in Modal Logic (AiML\u201922), S. Pinchinat D. Fern\u00e1ndez-Duque, A. Palmigiano (Ed.), Vol. AiML14. College Publications, 643\u2013657."},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.4324\/9780203252642"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005298632302"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005228629540"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1193667706"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1191333839"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1280-4"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0387-2_2"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632526","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632526","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:01Z","timestamp":1750178161000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632526"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,17]]},"references-count":66,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3632526"],"URL":"https:\/\/doi.org\/10.1145\/3632526","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,1,17]]},"assertion":[{"value":"2022-10-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-10","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}