{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:48:44Z","timestamp":1781927324216,"version":"3.54.5"},"reference-count":27,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T00:00:00Z","timestamp":1305590400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call \"shallow calculi\", where inference rules are only applied at the root node in a nested sequent. Our shallow calculi are extensions of Kashima's calculus for tense logic and share an essential characteristic with display calculi, namely, the presence of structural rules called \"display postulates\". Shallow calculi enjoy a simple cut elimination procedure, but are unsuitable for proof search due to the presence of display postulates and other structural rules. The second style of calculi uses deep-inference, whereby inference rules can be applied at any node in a nested sequent. We show that, for a range of extensions of tense logic, the two styles of calculi are equivalent, and there is a natural proof theoretic correspondence between display postulates and deep inference. The deep inference calculi enjoy the subformula property and have no display postulates or other structural rules, making them a better framework for proof search.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:8)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":24,"title":["On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"given":"Rajeev","family":"Gore","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Linda","family":"Postniece","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alwen F","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2011,5,17]]},"reference":[{"key":"10.2168\/LMCS-7(2:8)2011_aczel-handbook","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"issue":"2","key":"10.2168\/LMCS-7(2:8)2011_arecesbernardi2004","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1023\/B:JLLI.0000024730.34743.fa","volume":"13","author":"Carlos Areces and Raffaella Bernardi","year":"2004","journal-title":"Journal of Logic, Language, and Information 2004"},{"key":"10.2168\/LMCS-7(2:8)2011_Belnap82JPL","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"Nuel Belnap","year":"1982","journal-title":"Journal of Philosophical Logic"},{"key":"10.2168\/LMCS-7(2:8)2011_brunnler2006","unstructured":"Kai Br\u00fcnnler. Deep sequent systems for modal logic. In G. Governatori et al, editor,Advances in Modal Logic 6, pages 107-119. College Publications, 2006."},{"issue":"6","key":"10.2168\/LMCS-7(2:8)2011_Brunnler09AML","doi-asserted-by":"crossref","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"Kai Br\u00fcnnler","year":"2009","journal-title":"Archive for Mathematical Logic"},{"key":"10.2168\/LMCS-7(2:8)2011_BruHabil","unstructured":"Kai Br\u00fcnnler. Nested sequents.CoRR, abs\/1004.1845, 2010."},{"key":"10.2168\/LMCS-7(2:8)2011_Brunnler09tableaux","doi-asserted-by":"crossref","unstructured":"Kai Br\u00fcnnler and Lutz Stra\u00dfburger. Modular sequent systems for modal logic. In Giese and Waaler tableaux2009, pages 152-166.","DOI":"10.1007\/978-3-642-02716-1_12"},{"key":"10.2168\/LMCS-7(2:8)2011_Brunnler01LPAR","doi-asserted-by":"crossref","unstructured":"Kai Br\u00fcnnler and Alwen Tiu. A local system for classical logic. InLPAR, volume 2250 ofLecture Notes in Computer Science, pages 347-361. Springer, 2001.","DOI":"10.1007\/3-540-45653-8_24"},{"issue":"3-4","key":"10.2168\/LMCS-7(2:8)2011_CaFa-De-CeGa.ea97","doi-asserted-by":"crossref","first-page":"281","DOI":"10.3233\/FI-1997-323404","volume":"32","author":"Marcos A. Castilho, Luis Fari\u00f1as del Cer","year":"1997","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-7(2:8)2011_tableaux2009","unstructured":"Martin Giese and Arild Waaler, editors.Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings, volume 5607 ofLecture Notes in Computer Science. Springer, 2009. Seymour Ginsburg.The Mathematical Theory of Context-Free Languages. McGraw-Hill, Inc., New York, NY, USA, 1966."},{"issue":"3","key":"10.2168\/LMCS-7(2:8)2011_Gore98IGPL","first-page":"451","volume":"6","author":"Rajeev Gor\u00e9","year":"1998","journal-title":"LJIGPL"},{"key":"10.2168\/LMCS-7(2:8)2011_Gore09tableaux","doi-asserted-by":"crossref","unstructured":"Rajeev Gor\u00e9, Linda Postniece, and Alwen Tiu. Taming displayed tense logics using nested sequents with deep inference. In Giese and Waaler tableaux2009, pages 189-204.","DOI":"10.1007\/978-3-642-02716-1_15"},{"issue":"4","key":"10.2168\/LMCS-7(2:8)2011_Gore07JLC","doi-asserted-by":"crossref","first-page":"767","DOI":"10.1093\/logcom\/exm026","volume":"17","author":"Rajeev Gor\u00e9 and Alwen Tiu","year":"2007","journal-title":"J. Log. Comput."},{"key":"10.2168\/LMCS-7(2:8)2011_heuerding1998","doi-asserted-by":"crossref","unstructured":"Alain Heuerding, Michael Seyfried, and Heinrich Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. InTABLEAUX, volume 1071 ofLNCS, pages 210-225. Springer, 1996.","DOI":"10.1007\/3-540-61208-4_14"},{"key":"10.2168\/LMCS-7(2:8)2011_indrzejczak-multiple-sequent-tense","unstructured":"Andrzej Indrzejczak. Multiple sequent calculus for tense logics. International Conference on Temporal Logic, Leipzig 2000. 93-104."},{"key":"10.2168\/LMCS-7(2:8)2011_kashima-cut-free-tense","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF01053026","volume":"53","author":"Ryo Kashima","year":"1994","journal-title":"Studia Logica"},{"key":"10.2168\/LMCS-7(2:8)2011_kracht-power","doi-asserted-by":"crossref","unstructured":"Marcus Kracht. Power and weakness of the modal display calculus. In Heinrich Wansing, editor,Proof Theory of Modal Logics, pages 92-121. Kluwer, 1996.","DOI":"10.1007\/978-94-017-2798-3_7"},{"key":"10.2168\/LMCS-7(2:8)2011_lamarche","unstructured":"Francois Lamarche. On the algebra of structural contexts. Accepted atMathematical Structures in Computer Science, 2007."},{"key":"10.2168\/LMCS-7(2:8)2011_Lemmon77","unstructured":"Edward John Lemmon and Dana S. Scott.An Introduction to Modal Logic. Blackwell, Oxford, 1977."},{"issue":"5-6","key":"10.2168\/LMCS-7(2:8)2011_negri2005","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"Sara Negri","year":"2005","journal-title":"JPL"},{"key":"10.2168\/LMCS-7(2:8)2011_Papadimitriou","unstructured":"Christos H. Papadimitriou.Computational Complexity. Addison-Wesley Publishing Company, Inc., USA, 1994."},{"key":"10.2168\/LMCS-7(2:8)2011_poggiolesi2009","doi-asserted-by":"crossref","unstructured":"Francesca Poggiolesi. The tree-hypersequent method for modal propositional logic.Trends in Logic: Towards Mathematical Philsophy, pages 9-30, 2009.","DOI":"10.1007\/978-90-481-9670-8_6"},{"key":"10.2168\/LMCS-7(2:8)2011_Postniece10Phd","unstructured":"Linda Postniece.Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic. PhD thesis, The Australian National University, 2011."},{"key":"10.2168\/LMCS-7(2:8)2011_Sadrzadeh10","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1017\/S1755020310000134","volume":"3","author":"Mehrnoosh Sadrzadeh and Roy Dyckhoff","year":"2010","journal-title":"Review of Symbolic Logic"},{"key":"10.2168\/LMCS-7(2:8)2011_Troelstra96bpt","unstructured":"Anne S. Troelstra and Helmut Schwichtenberg.Basic Proof Theory. Cambridge University Press, 1996."},{"issue":"2","key":"10.2168\/LMCS-7(2:8)2011_trzesicki-gentzen-tense-logic","first-page":"75","volume":"13","author":"Kazimierz Trzesicki","year":"1984","journal-title":"Bulleting of the Section of Logic"},{"key":"10.2168\/LMCS-7(2:8)2011_wansing98","doi-asserted-by":"crossref","unstructured":"Heinrich Wansing.Displaying Modal Logic. Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-1280-4"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/971\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/971\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T21:26:13Z","timestamp":1741728373000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/971"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,17]]},"references-count":27,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:8)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1103.5286","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1103.5286","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,17]]},"article-number":"971"}}