{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T06:46:47Z","timestamp":1791442007177,"version":"4.3.3"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T00:00:00Z","timestamp":1624838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,7,30]]},"abstract":"<jats:p>We extend to natural deduction the approach of Linear Nested Sequents and of 2-Sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction: only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (\u00e0 la Scott) for formulating sound deduction rules.<\/jats:p>","DOI":"10.1145\/3461661","type":"journal-article","created":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T13:07:55Z","timestamp":1624885675000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["From 2-Sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9834-1940","authenticated-orcid":false,"given":"Simone","family":"Martini","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Bologna and INRIA Sophia-Antipolis, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2466-0631","authenticated-orcid":false,"given":"Andrea","family":"Masini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3285-9827","authenticated-orcid":false,"given":"Margherita","family":"Zorzi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,28]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"We Will Show Them! Essays in Honour of Dov Gabbay, Sergei N. Art\u00ebmov, Howard Barringer, Artur S. d\u2019Avila Garcez, Lu\u00eds C","author":"Baaz Mathias","unstructured":"Mathias Baaz and Rosalie Iemhoff . 2005. On the proof theory of the existence predicate . In We Will Show Them! Essays in Honour of Dov Gabbay, Sergei N. Art\u00ebmov, Howard Barringer, Artur S. d\u2019Avila Garcez, Lu\u00eds C . Lamb, and John Woods (Eds.). College Publications , London, U.K. , 125\u2013166. Mathias Baaz and Rosalie Iemhoff. 2005. On the proof theory of the existence predicate. In We Will Show Them! Essays in Honour of Dov Gabbay, Sergei N. Art\u00ebmov, Howard Barringer, Artur S. d\u2019Avila Garcez, Lu\u00eds C. Lamb, and John Woods (Eds.). College Publications, London, U.K., 125\u2013166."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00021-6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200310096"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-004-0237-z"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2013.830401"},{"key":"e_1_2_1_6_1","first-page":"1","article-title":"A two-dimensional metric temporal logic","volume":"13","author":"Baratella Stefano","year":"2019","unstructured":"Stefano Baratella and Andrea Masini . 2019 . A two-dimensional metric temporal logic . Mathematical Logic Quarterly 13 (2019), 1 \u2013 13 . DOI:https:\/\/doi.org\/10.1002\/malq.201700036 10.1002\/malq.201700036 Stefano Baratella and Andrea Masini. 2019. A two-dimensional metric temporal logic. Mathematical Logic Quarterly 13 (2019), 1\u201313. DOI:https:\/\/doi.org\/10.1002\/malq.201700036","journal-title":"Mathematical Logic Quarterly"},{"key":"e_1_2_1_7_1","volume-title":"Proof Theory and Logical Complexity. Studies in Proof Theory. Monographs","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard . 1987. Proof Theory and Logical Complexity. Studies in Proof Theory. Monographs , Vol. 1 . Bibliopolis , Naples . 505 pages. Jean-Yves Girard. 1987. Proof Theory and Logical Complexity. Studies in Proof Theory. Monographs, Vol. 1. Bibliopolis, Naples. 505 pages."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.735"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00094-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00162-1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_10"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3288757"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3288757"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/212876.212892"},{"key":"e_1_2_1_16_1","volume-title":"Proof Theory of Modal Logics","author":"Martini Simone","unstructured":"Simone Martini and Andrea Masini . 1996. A computational interpretation of modal proofs . In Proof Theory of Modal Logics , H. Wansing (Ed.). Kluwer , Dordrecht , 213\u2013241. Simone Martini and Andrea Masini. 1996. A computational interpretation of modal proofs. In Proof Theory of Modal Logics, H. Wansing (Ed.). Kluwer, Dordrecht, 213\u2013241."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90029-Y"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.5.533"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.20.241-277"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2010.04.014"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq028"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2008.36"},{"key":"e_1_2_1_23_1","first-page":"5","article-title":"Modal deduction systems for quantum state transformations","volume":"17","author":"Masini Andrea","year":"2011","unstructured":"Andrea Masini , Luca Vigan\u00f2 , and Margherita Zorzi . 2011 . Modal deduction systems for quantum state transformations . Journal of Multiple-Valued Logic and Soft Computing 17 , 5 \u2013 6 (2011), 475\u2013519. Andrea Masini, Luca Vigan\u00f2, and Margherita Zorzi. 2011. Modal deduction systems for quantum state transformations. Journal of Multiple-Valued Logic and Soft Computing 17, 5\u20136 (2011), 475\u2013519.","journal-title":"Journal of Multiple-Valued Logic and Soft Computing"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1747-9991.2011.00418.x"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_9"},{"key":"e_1_2_1_26_1","volume-title":"Natural Deduction. A Proof-Theoretical Study. Almqvist & Wiksell","author":"Prawitz Dag","unstructured":"Dag Prawitz . 1965. Natural Deduction. A Proof-Theoretical Study. Almqvist & Wiksell , Stockholm . Dag Prawitz. 1965. Natural Deduction. A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061839"},{"key":"e_1_2_1_29_1","volume-title":"Constructivism in Mathematics (2 volumes). North-Holland","author":"Troelstra Anne Sjerp","unstructured":"Anne Sjerp Troelstra and Dirk van Dalen . 1988. Constructivism in Mathematics (2 volumes). North-Holland , Amsterdam . Anne Sjerp Troelstra and Dirk van Dalen. 1988. Constructivism in Mathematics (2 volumes). North-Holland, Amsterdam."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3461661","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3461661","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:05Z","timestamp":1750193345000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3461661"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,28]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,30]]}},"alternative-id":["10.1145\/3461661"],"URL":"https:\/\/doi.org\/10.1145\/3461661","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,28]]},"assertion":[{"value":"2020-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}