{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T12:53:51Z","timestamp":1763643231132,"version":"3.41.0"},"reference-count":34,"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"}],"funder":[{"name":"European Union\u2019s Horizon 2020","award":["689176"],"award-info":[{"award-number":["689176"]}]},{"name":"FWF Projects","award":["START Y544-N23, I2982, W1255-N23, and P33548"],"award-info":[{"award-number":["START Y544-N23, I2982, W1255-N23, and P33548"]}]},{"name":"CogniGron research center"},{"name":"Ubbo Emmius Funds"}],"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 introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.<\/jats:p>","DOI":"10.1145\/3460492","type":"journal-article","created":{"date-parts":[[2021,6,28]],"date-time":"2021-06-28T13:07:55Z","timestamp":1624885675000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Display to Labeled Proofs and Back Again for Tense Logics"],"prefix":"10.1145","volume":"22","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Wien, Wien, Austria"}]},{"given":"Tim S.","family":"Lyon","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Dresden, Dresden, Germany"}]},{"given":"Revantha","family":"Ramanayake","sequence":"additional","affiliation":[{"name":"University of Groningen, Groningen, Netherlands"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"The Australian National University, Canberra, ACT, Australia"}]}],"member":"320","published-online":{"date-parts":[[2021,6,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00284976"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3381089.3381193"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Conference of the Italian Society for Logic and Philosophy of Science (SILFS\u201907)","author":"Boretti Bianca","year":"2009","unstructured":"Bianca Boretti and Sara Negri . 2009 . On the finitization of Priorean linear time . In Proceedings of the International Conference of the Italian Society for Logic and Philosophy of Science (SILFS\u201907) . College Publications. Bianca Boretti and Sara Negri. 2009. On the finitization of Priorean linear time. In Proceedings of the International Conference of the Italian Society for Logic and Philosophy of Science (SILFS\u201907). College Publications."},{"key":"e_1_2_1_5_1","first-page":"107","article-title":"Deep sequent systems for modal logic. In Advances in Modal Logic. Vol. 6","author":"Br\u00fcnnler Kai","year":"2006","unstructured":"Kai Br\u00fcnnler . 2006 . Deep sequent systems for modal logic. In Advances in Modal Logic. Vol. 6 . Coll. Publ., London , 107 \u2013 119 . Kai Br\u00fcnnler. 2006. Deep sequent systems for modal logic. In Advances in Modal Logic. Vol. 6. Coll. Publ., London, 107\u2013119.","journal-title":"Coll. Publ., London"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19920380107"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379465.2379469"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370331"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72056-2_8"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2874775"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-011-0254-7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2015.7"},{"volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting Melvin","key":"e_1_2_1_13_1","unstructured":"Melvin Fitting . 1983. Proof Methods for Modal and Intuitionistic Logics . Synthese Library, Vol . 169. D. Reidel Publishing , Dordrecht. viii+555 pages. Melvin Fitting. 1983. Proof Methods for Modal and Intuitionistic Logics. Synthese Library, Vol. 169. D. Reidel Publishing, Dordrecht. viii+555 pages."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.004"},{"volume-title":"Labelled Deductive Systems. Oxford Logic guides","author":"Gabbay Dov M","key":"e_1_2_1_15_1","unstructured":"Dov M Gabbay . 1996. Labelled Deductive Systems. Oxford Logic guides , Vol. 33 . Clarendon Press\/Oxford Science Publications . Dov M Gabbay. 1996. Labelled Deductive Systems. Oxford Logic guides, Vol. 33. Clarendon Press\/Oxford Science Publications."},{"key":"e_1_2_1_16_1","volume-title":"Modal Logic for Philosophers","author":"Garson James W.","unstructured":"James W. Garson . 2013. Modal Logic for Philosophers ( 2 nd ed.). Cambridge University Press . DOI:https:\/\/doi.org\/10.1017\/CBO9781139342117 10.1017\/CBO9781139342117 James W. Garson. 2013. Modal Logic for Philosophers (2nd ed.). Cambridge University Press. DOI:https:\/\/doi.org\/10.1017\/CBO9781139342117","edition":"2"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Jean-Yves Girard. 1989. Towards a geometry of interaction. In Categories in Computer Science and Logic. AMS 69\u2013108.  Jean-Yves Girard. 1989. Towards a geometry of interaction. In Categories in Computer Science and Logic. AMS 69\u2013108.","DOI":"10.1090\/conm\/092\/1003197"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.3.451"},{"key":"e_1_2_1_19_1","volume-title":"On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7, 2","author":"Gor\u00e9 Rajeev","year":"2011","unstructured":"Rajeev Gor\u00e9 , Linda Postniece , and Alwen Tiu . 2011. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7, 2 ( 2011 ), 2:8, 38. Rajeev Gor\u00e9, Linda Postniece, and Alwen Tiu. 2011. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7, 2 (2011), 2:8, 38."},{"key":"e_1_2_1_20_1","volume-title":"Advances in Modal Logic","volume":"9","author":"Gor\u00e9 Rajeev","year":"2012","unstructured":"Rajeev Gor\u00e9 and Revantha Ramanayake . 2012 . Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents . In Advances in Modal Logic , vol. 9 . College Publications. Rajeev Gor\u00e9 and Revantha Ramanayake. 2012. Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents. In Advances in Modal Logic, vol. 9. College Publications."},{"key":"e_1_2_1_21_1","first-page":"1367","article-title":"Unified correspondence as a proof-theoretic tool","volume":"28","author":"Greco Giuseppe","year":"2016","unstructured":"Giuseppe Greco , Minghui Ma , Alessandra Palmigiano , Apostolos Tzimoulis , and Zhiguang Zhao . 2016 . Unified correspondence as a proof-theoretic tool . J. Logic Comput. 28 , 7 (2016), 1367 \u2013 1442 . DOI: DOI:10.1093\/logcom\/exw022 10.1093\/logcom Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Apostolos Tzimoulis, and Zhiguang Zhao. 2016. Unified correspondence as a proof-theoretic tool. J. Logic Comput. 28, 7 (2016), 1367\u20131442. DOI: DOI:10.1093\/logcom\/exw022","journal-title":"J. Logic Comput."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/646560.695248"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053026"},{"key":"e_1_2_1_24_1","volume-title":"Proof Theory of Modal Logic (Hamburg","author":"Kracht Marcus","year":"1993","unstructured":"Marcus Kracht . 1996. Power and weakness of the modal display calculus . In Proof Theory of Modal Logic (Hamburg , 1993 ). Appl. Log. Ser., Vol. 2 . Kluwer Academic Publishers , Dordrecht, 93\u2013121. Marcus Kracht. 1996. Power and weakness of the modal display calculus. In Proof Theory of Modal Logic (Hamburg, 1993). Appl. Log. Ser., Vol. 2. Kluwer Academic Publishers, Dordrecht, 93\u2013121."},{"key":"e_1_2_1_25_1","article-title":"On the correspondence between nested calculi and semantic systems for intuitionistic logics","volume":"31","author":"Lyon Tim","year":"2020","unstructured":"Tim Lyon . 2020 . On the correspondence between nested calculi and semantic systems for intuitionistic logics . J. Logic Comput. 31 , 1 (12 2020), 213\u2013265. DOI:https:\/\/doi.org\/10.1093\/logcom\/exaa078 arXiv:https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/1\/213\/36677523\/exaa078.pdf. 10.1093\/logcom Tim Lyon. 2020. On the correspondence between nested calculi and semantic systems for intuitionistic logics. J. Logic Comput. 31, 1 (12 2020), 213\u2013265. DOI:https:\/\/doi.org\/10.1093\/logcom\/exaa078 arXiv:https:\/\/academic.oup.com\/logcom\/article-pdf\/31\/1\/213\/36677523\/exaa078.pdf.","journal-title":"J. Logic Comput."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920)","volume":"152","author":"Lyon Tim","year":"2020","unstructured":"Tim Lyon , Alwen Tiu , Rajeev Gor\u00e9 , and Ranald Clouston . 2020 . Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents . In Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920) (LIPIcs), Maribel Fern\u00e1ndez and Anca Muscholl (Eds.) , Vol. 152 . Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 28:1\u201328:16. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.28 10.4230\/LIPIcs.CSL.2020.28 Tim Lyon, Alwen Tiu, Rajeev Gor\u00e9, and Ranald Clouston. 2020. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Proceedings of the 28th EACSL Annual Conference on Computer Science Logic (CSL\u201920) (LIPIcs), Maribel Fern\u00e1ndez and Anca Muscholl (Eds.), Vol. 152. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 28:1\u201328:16. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.28"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33792-6_13"},{"volume-title":"Proceedings of the IEEE International Workshop on Advances in Artificial Intelligence & Machine Learning (AiML\u201914)","author":"Marin S.","key":"e_1_2_1_28_1","unstructured":"S. Marin and L. Strassburger . 2014. Label-free modular systems for classical and intuitionistic modal logics . In Proceedings of the IEEE International Workshop on Advances in Artificial Intelligence & Machine Learning (AiML\u201914) (LNCS). Springer. S. Marin and L. Strassburger. 2014. Label-free modular systems for classical and intuitionistic modal logics. In Proceedings of the IEEE International Workshop on Advances in Artificial Intelligence & Machine Learning (AiML\u201914) (LNCS). Springer."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1017948105274"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"volume-title":"A semantical view of proof systems","author":"Pimentel Elaine","key":"e_1_2_1_31_1","unstructured":"Elaine Pimentel . 2018. A semantical view of proof systems . In Logic, Language, Information, and Computation, Lawrence S. Moss, Ruy de Queiroz, and Maricarmen Martinez (Eds.). Springer , Berlin , 61\u201376. Elaine Pimentel. 2018. A semantical view of proof systems. In Logic, Language, Information, and Computation, Lawrence S. Moss, Ruy de Queiroz, and Maricarmen Martinez (Eds.). Springer, Berlin, 61\u201376."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9425-4"},{"key":"e_1_2_1_33_1","unstructured":"George Rebane and Judea Pearl. 2013. The recovery of causal poly-trees from statistical data. Retrieved from https:\/\/arXiv:1304.2736.  George Rebane and Judea Pearl. 2013. The recovery of causal poly-trees from statistical data. Retrieved from https:\/\/arXiv:1304.2736."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3208-5"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/298610"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460492","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460492","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:55Z","timestamp":1750193275000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460492"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,28]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,30]]}},"alternative-id":["10.1145\/3460492"],"URL":"https:\/\/doi.org\/10.1145\/3460492","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,6,28]]},"assertion":[{"value":"2020-01-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"}}]}}