{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:23Z","timestamp":1759017923480,"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>We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_22","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:15Z","timestamp":1758969915000},"page":"414-432","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Intuitionistic BV"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0425-2825","authenticated-orcid":false,"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4661-6540","authenticated-orcid":false,"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Horne, R., Mauw, S., Stra\u00dfburger, L.: A graphical proof theory of logical time. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0228, pp. 22:1\u201322:25. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2022). https:\/\/doi.org\/10.4230\/lipics.fscd.2022.22","DOI":"10.4230\/lipics.fscd.2022.22"},{"key":"22_CR2","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Manara, G.: Proofs as execution trees for the $$\\pi $$-calculus. arXiv eprint 2411.08847 [cs.LO] (2024). https:\/\/doi.org\/10.48550\/arXiv.2411.08847","DOI":"10.48550\/arXiv.2411.08847"},{"key":"22_CR3","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Manara, G., Montesi, F.: Formulas as processes, deadlock-freedom as choreographies. In: Vafeiadis, V. (ed.) ESOP 2025. LNCS, vol. 15694, pp. 23\u201355. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_2","DOI":"10.1007\/978-3-031-91118-7_2"},{"key":"22_CR4","doi-asserted-by":"publisher","unstructured":"Acclavio, M., Stra\u00dfburger, L.: Intuitionistic BV (extended version). arXiv eprint 2505.13284 [cs.LO] (2025). https:\/\/doi.org\/10.48550\/arXiv.2505.13284","DOI":"10.48550\/arXiv.2505.13284"},{"issue":"3","key":"22_CR5","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10485-010-9241-0","volume":"20","author":"R Blute","year":"2012","unstructured":"Blute, R., Panangaden, P., Slavnov, S.: Deep inference and probabilistic coherence spaces. Appl. Categ. Struct. 20(3), 209\u2013228 (2012). https:\/\/doi.org\/10.1007\/s10485-010-9241-0","journal-title":"Appl. Categ. Struct."},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45653-8_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Br\u00fcnnler","year":"2001","unstructured":"Br\u00fcnnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347\u2013361. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45653-8_24"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45619-8_21","volume-title":"Logic Programming","author":"P Bruscoli","year":"2002","unstructured":"Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 302\u2013316. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45619-8_21"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Cockett, J.R.B., Seely, R.A.G.: Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory Appl. Categ. 3(5), 85\u2013131 (1997). http:\/\/www.tac.mta.ca\/tac\/volumes\/1997\/n5\/3-05abs.html","DOI":"10.70930\/tac\/y384e20i"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Guglielmi, A.: Concurrency and plan generation in a logic programming language with a sequential operator. In: van Hentenryck, P. (ed.) Logic Programming: 11th International Conference, pp. 240\u2013254. MIT Press, Cambridge (1994). https:\/\/doi.org\/10.7551\/mitpress\/4316.003.0030","DOI":"10.7551\/mitpress\/4316.003.0030"},{"key":"22_CR10","doi-asserted-by":"publisher","unstructured":"Guglielmi, A.: Sequentiality by linear implication and universal quantification. In: Desel, J. (ed.) Structures in Concurrency Theory. Workshops in Computing, pp. 160\u2013174. Springer, London (1995). https:\/\/doi.org\/10.1007\/978-1-4471-3078-9_11","DOI":"10.1007\/978-1-4471-3078-9_11"},{"key":"22_CR11","doi-asserted-by":"publisher","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1) (2007). https:\/\/doi.org\/10.1145\/1182613.1182614","DOI":"10.1145\/1182613.1182614"},{"key":"22_CR12","doi-asserted-by":"publisher","unstructured":"Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: Lynch, C. (ed.) 21st International Conference on Rewriting Techniques and Applications (RTA 2010). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a06, pp. 135\u2013150. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2010). https:\/\/doi.org\/10.4230\/lipics.rta.2010.135","DOI":"10.4230\/lipics.rta.2010.135"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-44802-0_5","volume-title":"Computer Science Logic","author":"A Guglielmi","year":"2001","unstructured":"Guglielmi, A., Stra\u00dfburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54\u201368. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_5"},{"issue":"3","key":"22_CR14","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1017\/s096012951100003x","volume":"21","author":"A Guglielmi","year":"2011","unstructured":"Guglielmi, A., Stra\u00dfburger, L.: A system of interaction and structure V: the exponentials and splitting. Math. Struct. Comput. Sci. 21(3), 563\u2013584 (2011). https:\/\/doi.org\/10.1017\/s096012951100003x","journal-title":"Math. Struct. Comput. Sci."},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Horne, R., Tiu, A., Aman, B., Ciobanu, G.: Private names in non-commutative logic. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a059, pp. 31:1\u201331:16. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2016). https:\/\/doi.org\/10.4230\/lipics.concur.2016.31","DOI":"10.4230\/lipics.concur.2016.31"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Horne, R., Tiu, A., Aman, B., Ciobanu, G.: De Morgan dual nominal quantifiers modelling private names in non-commutative logic. ACM Trans. Comput. Logic 20(4), 22:1\u201322:44 (2019). https:\/\/doi.org\/10.1145\/3325821","DOI":"10.1145\/3325821"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"986","DOI":"10.1007\/978-3-540-30182-0_99","volume-title":"Computer and Information Sciences - ISCIS 2004","author":"O Kahramano\u011fullar\u0131","year":"2004","unstructured":"Kahramano\u011fullar\u0131, O.: System BV without the Equalities for Unit. In: Aykanat, C., Dayar, T., K\u00f6rpeo\u011flu, \u0130 (eds.) ISCIS 2004. LNCS, vol. 3280, pp. 986\u2013995. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30182-0_99"},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Nguy\u00ean, L.T.D., Stra\u00dfburger, L.: A system of interaction and structure III: the complexity of BV and pomset logic. Log. Methods Comput. Sci. 19(4), 25:1\u201325:60 (2023). https:\/\/doi.org\/10.46298\/lmcs-19(4:25)2023","DOI":"10.46298\/lmcs-19(4:25)2023"},{"key":"22_CR19","doi-asserted-by":"publisher","unstructured":"Nguy\u00ean, L.T.D., Stra\u00dfburger, L.: BV and pomset logic are not the same. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0216, pp. 3:1\u20133:17. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2022). https:\/\/doi.org\/10.4230\/lipics.csl.2022.3","DOI":"10.4230\/lipics.csl.2022.3"},{"key":"22_CR20","unstructured":"Retor\u00e9, C.: R\u00e9seaux et s\u00e9quents ordonn\u00e9s. Ph.D. thesis, Universit\u00e9 Paris VII (1993)"},{"key":"22_CR21","unstructured":"Retor\u00e9, C.: Pomset logic as a calculus of directed cographs. In: Abrusci, V.M., Casadio, C. (eds.) Dynamic Perspectives in Logic and Linguistics, pp. 221\u2013247. Bulzoni Editore, Roma (1999). Also available as INRIA Rapport de Recherche RR-3714"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Retor\u00e9, C.: Pomset logic: the other approach to noncommutativity in logic. In: Casadio, C., Scott, P.J. (eds.) Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Outstanding Contributions to Logic, vol.\u00a020, pp. 299\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-66545-6_9","DOI":"10.1007\/978-3-030-66545-6_9"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-21691-6_16","volume-title":"Typed Lambda Calculi and Applications","author":"L Roversi","year":"2011","unstructured":"Roversi, L.: Linear lambda calculus and deep inference. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 184\u2013197. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21691-6_16"},{"key":"22_CR24","doi-asserted-by":"publisher","unstructured":"Simmons, W., Kissinger, A.: Higher-order causal theories are models of BV-logic. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0241, pp. 80:1\u201380:14. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2022). https:\/\/doi.org\/10.4230\/lipics.mfcs.2022.80","DOI":"10.4230\/lipics.mfcs.2022.80"},{"key":"22_CR25","unstructured":"Stra\u00dfburger, L.: Linear logic and noncommutativity in the calculus of structures. Ph.D. thesis, Technische Universit\u00e4t Dresden (2003)"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Tiu, A.: A system of interaction and structure II: the need for deep inference. Log. Methods Comput. Sci. 2(2), 4:1\u20134:24 (2006). https:\/\/doi.org\/10.2168\/lmcs-2(2:4)2006","DOI":"10.2168\/lmcs-2(2:4)2006"}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:16Z","timestamp":1758969916000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_22"}},"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_22","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"}}]}}