{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:20Z","timestamp":1759017920406,"version":"3.44.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a formalization of the nonassociative Lambek calculus in the Agda proof assistant. The sequent calculus for this logic has sequents with binary trees as antecedents, in which formulae are stored as leaves. The shape of the antecedents creates subtleties when proving logical properties, since in many cases one needs to analyze equalities involving sequentially-composed trees. We formally characterize these equalities and show how to employ the resulting technical lemma to prove cut admissibility and the Maehara interpolation properly, which implies Craig interpolation. We show that both the cut rule and the interpolation procedure are well-defined wrt. a certain notion of equivalence of derivations. We additionally prove a proof-relevant version of Maehara interpolation, exhibiting the interpolation procedure as a right inverse of the admissible cut rule.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_23","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:24Z","timestamp":1758969924000},"page":"433-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Agda Formalization of\u00a0Nonassociative Lambek Calculus and\u00a0its Metatheory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7230-3436","authenticated-orcid":false,"given":"Niccol\u00f2","family":"Veltri","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2053-1688","authenticated-orcid":false,"given":"Cheng-Syuan","family":"Wan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"issue":"3","key":"23_CR1","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1017\/s175502031400015x","volume":"7","author":"M Alizadeh","year":"2014","unstructured":"Alizadeh, M., Derakhshan, F., Ono, H.: Uniform interpolation in substructural logics. Rev. Symb. Log. 7(3), 455\u2013483 (2014). https:\/\/doi.org\/10.1017\/s175502031400015x","journal-title":"Rev. Symb. Log."},{"key":"23_CR2","unstructured":"Anoun, H., Cast\u00e9ran, P., Moot, R.: Proof automation for type-logical grammars. Lecture notes for ESSLLI 2004 (2004). https:\/\/www.labri.fr\/perso\/moot\/esslli_reader.pdf, https:\/\/github.com\/rocq-archive\/lambek"},{"issue":"7\u20138","key":"23_CR3","first-page":"507","volume":"34","author":"W Buszkowski","year":"1986","unstructured":"Buszkowski, W.: Generative capacity of nonassociative Lambek calculus. Bull. Pol. Acad. Sci. Math. 34(7\u20138), 507\u2013516 (1986)","journal-title":"Bull. Pol. Acad. Sci. Math."},{"issue":"3","key":"23_CR4","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1093\/jigpal\/jzp094","volume":"19","author":"W Buszkowski","year":"2010","unstructured":"Buszkowski, W.: Interpolation and FEP for logics of residuated algebras. Log. J. IGPL 19(3), 437\u2013454 (2010). https:\/\/doi.org\/10.1093\/jigpal\/jzp094","journal-title":"Log. J. IGPL"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-01748-3_4","volume-title":"Languages: From Formal to Natural","author":"W Buszkowski","year":"2009","unstructured":"Buszkowski, W., Farulewski, M.: Nonassociative Lambek calculus with additives and context-free languages. In: Grumberg, O., Kaminski, M., Katz, S., Wintner, S. (eds.) Languages: From Formal to Natural. LNCS, vol. 5533, pp. 45\u201358. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01748-3_4"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-540-85110-3_5","volume-title":"Intelligent Computer Mathematics","author":"P Chapman","year":"2008","unstructured":"Chapman, P., McKinna, J., Urban, C.: Mechanising a proof of Craig\u2019s interpolation theorem for intuitionistic logic in nominal isabelle. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 38\u201352. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85110-3_5"},{"issue":"3","key":"23_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269\u2013285 (1957). https:\/\/doi.org\/10.2307\/2963594","journal-title":"J. Symb. Log."},{"key":"23_CR8","unstructured":"\u010cubri\u0107, D.: Results in categorical proof theory. Ph.D. thesis, McGill University (1993). https:\/\/escholarship.mcgill.ca\/concern\/theses\/pv63g1818"},{"issue":"4","key":"23_CR9","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/bf01270628","volume":"33","author":"D \u010cubri\u0107","year":"1994","unstructured":"\u010cubri\u0107, D.: Interpolation property for bicartesian closed categories. Arch. Math. Log. 33(4), 291\u2013319 (1994). https:\/\/doi.org\/10.1007\/bf01270628","journal-title":"Arch. Math. Log."},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"F\u00e9r\u00e9e, H., van\u00a0der Giessen, I., van Gool, S., Shillito, I.: Mechanised uniform interpolation for modal logics K, GL, and iSL. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14740, pp. 43\u201360. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_3","DOI":"10.1007\/978-3-031-63501-4_3"},{"key":"23_CR11","doi-asserted-by":"publisher","unstructured":"F\u00e9r\u00e9e, H., van Gool, S.: Formalizing and computing propositional quantifiers. In: Krebbers, R., Traytel, D., Pientka, B., Zdancewic, S. (eds.) Proceedings of 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pp. 148\u2013158. ACM (2023). https:\/\/doi.org\/10.1145\/3573105.3575668","DOI":"10.1145\/3573105.3575668"},{"issue":"1","key":"23_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/a:1026175817625","volume":"13","author":"G J\u00e4ger","year":"2004","unstructured":"J\u00e4ger, G.: Residuation, structural rules and context freeness. J. Log. Lang. Inf. 13(1), 47\u201359 (2004). https:\/\/doi.org\/10.1023\/a:1026175817625","journal-title":"J. Log. Lang. Inf."},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Kandulski, M.: The equivalence of nonassociative Lambek categorial grammars and context-free grammars. Z. Math. Log. Grundl. Math. 34(1) (1988). https:\/\/doi.org\/10.1002\/malq.19880340106","DOI":"10.1002\/malq.19880340106"},{"key":"23_CR14","unstructured":"Kokke, P.: Formalising type-logical grammars in Agda. In: Extended abstracts of the ESSLLI 2015 workshop TYTLES: Types Theory and Lexical Semantics, pp. 83\u201390 (2015). https:\/\/www.lirmm.fr\/tytles\/Articles\/Kokke.pdf, https:\/\/github.com\/wenkokke\/msla2014\/blob\/b880cf25ed8e81b9a965ea9aad18377008d68a9f\/src\/LambekGrishinCalculus.agda"},{"issue":"3","key":"23_CR15","doi-asserted-by":"publisher","first-page":"154","DOI":"10.2307\/2310058","volume":"65","author":"J Lambek","year":"1958","unstructured":"Lambek, J.: The mathematics of sentence structure. Amer. Math. Monthly 65(3), 154\u2013170 (1958). https:\/\/doi.org\/10.2307\/2310058","journal-title":"Amer. Math. Monthly"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Lambek, J.: On the calculus of syntactic types. In: Jakobson, R. (ed.) Structure of Language and Its Mathematical Aspects, Proceedings of Symposium in Applied Mathematics, vol.\u00a012, pp. 166\u2013178. American Mathematical Society, Providence (1961). https:\/\/doi.org\/10.1090\/psapm\/012","DOI":"10.1090\/psapm\/012"},{"issue":"3","key":"23_CR17","doi-asserted-by":"publisher","first-page":"494","DOI":"10.1093\/jigpal\/jzt042","volume":"22","author":"Z Lin","year":"2014","unstructured":"Lin, Z.: Non-associative Lambek calculus with modalities: interpolation, complexity and FEP. Log. J. IGPL 22(3), 494\u2013512 (2014). https:\/\/doi.org\/10.1093\/jigpal\/jzt042","journal-title":"Log. J. IGPL"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"Maehara, S.: Craig\u2019s interpolation theorem. S\u00fbgaku 12(4), 235\u2013237 (1961). https:\/\/doi.org\/10.11429\/sugaku1947.12.235","DOI":"10.11429\/sugaku1947.12.235"},{"key":"23_CR19","doi-asserted-by":"publisher","unstructured":"Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) Proceedings of 23rd International Conference on Types for Proofs and Programs (TYPES\u00a02017). Leibniz International Proceedings in Informatics, vol.\u00a0104, pp. 5:1\u20135:16. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2019). https:\/\/doi.org\/10.4230\/lipics.types.2017.5","DOI":"10.4230\/lipics.types.2017.5"},{"key":"23_CR20","doi-asserted-by":"publisher","unstructured":"Moot, R., Retore, C.: The Logic of Categorial Grammars: A Deductive Account of Natural Language Syntax and Semantics. LNCS, vol. 6850. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31555-8","DOI":"10.1007\/978-3-642-31555-8"},{"key":"23_CR21","doi-asserted-by":"publisher","unstructured":"Ono, H.: Proof-theoretic methods in nonclassical logic: an introduction. In: Dezani-Ciancaglini, M., Okada, M., Takahashi, M. (eds.) Theories of Types and Proofs. Mathematical Society Memoirs, vol.\u00a02, pp. 207\u2013254. Mathematical Society of Japan (1998). https:\/\/doi.org\/10.2969\/msjmemoirs\/00201c060","DOI":"10.2969\/msjmemoirs\/00201c060"},{"key":"23_CR22","doi-asserted-by":"publisher","unstructured":"Ridge, T.: Craig\u2019s interpolation theorem formalised and mechanised in Isabelle\/HOL. arXiv eprint arXiv:cs\/0607058 [cs.LO] (2006). https:\/\/doi.org\/10.48550\/arxiv.cs\/0607058","DOI":"10.48550\/arxiv.cs\/0607058"},{"key":"23_CR23","unstructured":"Roorda, D.: Resource logics: proof-theoretical investigations. Ph.D. thesis, Universiteit van Amsterdam (1991). https:\/\/pure.knaw.nl\/ws\/portalfiles\/portal\/1821261\/Roorda_1991_Resource_Logics_Proof_theoretical_Investigations.pdf"},{"key":"23_CR24","doi-asserted-by":"publisher","unstructured":"Saurin, A.: Interpolation as cut-introduction: on the computational content of Craig-Lyndon interpolation. In: Fern\u00e1ndez, M. (ed.) Proceedings of 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics, vol.\u00a0337, pp. 32:1\u201332:21. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2025). https:\/\/doi.org\/10.4230\/lipics.fscd.2025.32","DOI":"10.4230\/lipics.fscd.2025.32"},{"key":"23_CR25","doi-asserted-by":"publisher","unstructured":"Tian, C.: Formalized Lambek calculus in higher order logic HOL4. arXiv eprint arXiv:1705.07318 [cs.CL] (2017). https:\/\/doi.org\/10.48550\/arXiv.1705.07318, https:\/\/github.com\/binghe\/informatica-public\/tree\/master\/lambek","DOI":"10.48550\/arXiv.1705.07318"},{"key":"23_CR26","doi-asserted-by":"publisher","unstructured":"Veltri, N., Wan, C.-S.: Craig interpolation for a semi-substructural logic. Stud. Log. (to appear). https:\/\/doi.org\/10.1007\/s11225-025-10189-7","DOI":"10.1007\/s11225-025-10189-7"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:27Z","timestamp":1758969927000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}