{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T00:38:00Z","timestamp":1780447080811,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,2,17]],"date-time":"2016-02-17T00:00:00Z","timestamp":1455667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Austrian Science Fund (FWF), START","award":["Y544"],"award-info":[{"award-number":["Y544"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,7,22]]},"abstract":"<jats:p>What can (and cannot) be expressed by structural display rules? Given a display calculus, we present a systematic procedure for transforming axioms into structural rules. The conditions for the procedure are given in terms of (purely syntactic) abstract properties of the base calculus; thus, the method applies to large classes of calculi and logics. If the calculus satisfies certain additional properties, we prove the converse direction, thus characterising the class of axioms that can be captured by structural display rules. Determining if an axiom belongs to this class or not is shown to be decidable. Applied to the display calculus for tense logic, we obtain a new proof of Kracht\u2019s Display Theorem I.<\/jats:p>","DOI":"10.1145\/2874775","type":"journal-article","created":{"date-parts":[[2016,2,22]],"date-time":"2016-02-22T13:07:16Z","timestamp":1456146436000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Power and Limits of Structural Display Rules"],"prefix":"10.1145","volume":"17","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[{"name":"Vienna University of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Revantha","family":"Ramanayake","sequence":"additional","affiliation":[{"name":"Vienna University of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,2,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273828"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-003-1822-4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00284976"},{"key":"e_1_2_1_5_1","volume-title":"Modal Logic. Cambridge Tracts in Theoretical Computer Science","volume":"53","author":"Blackburn P.","unstructured":"P. Blackburn , M. de Rijke , and I. Venema . 2001 . Modal Logic. Cambridge Tracts in Theoretical Computer Science , Vol. 53 . Cambridge University Press, Cambridge, UK. P. Blackburn, M. de Rijke, and I. Venema. 2001. Modal Logic. Cambridge Tracts in Theoretical Computer Science, Vol. 53. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-012-9449-0"},{"key":"e_1_2_1_7_1","volume-title":"Advances in Modal Logic.","author":"Br\u00fcnnler K.","unstructured":"K. Br\u00fcnnler . 2006. Deep sequent systems for modal logic . In Advances in Modal Logic. Vol. 6 . College Publications , London , 107--119. K. Br\u00fcnnler. 2006. Deep sequent systems for modal logic. In Advances in Modal Logic. Vol. 6. College Publications, London, 107--119."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.39"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.003"},{"key":"e_1_2_1_10_1","volume-title":"WOLLIC","volume":"8071","author":"Ciabattoni A.","year":"2013","unstructured":"A. Ciabattoni and R. Ramanayake . 2013. Structural rule extensions of display calculi: A general recipe . In WOLLIC 2013 . Lecture Notes in Computer Science , Vol. 8071 . Springer, Berlin, 81--95. A. Ciabattoni and R. Ramanayake. 2013. Structural rule extensions of display calculi: A general recipe. In WOLLIC 2013. Lecture Notes in Computer Science, Vol. 8071. Springer, Berlin, 81--95."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-014-9566-z"},{"key":"e_1_2_1_12_1","volume-title":"Lecture Notes in Computer Science","volume":"5771","author":"Ciabattoni A.","unstructured":"A. Ciabattoni , L. Strassburger , and K. Terui . 2009. Expanding the realm of systematic proof theory. In Computer Science Logic 2009 . Lecture Notes in Computer Science , Vol. 5771 . Springer, Berlin, 163--178. A. Ciabattoni, L. Strassburger, and K. Terui. 2009. Expanding the realm of systematic proof theory. In Computer Science Logic 2009. Lecture Notes in Computer Science, Vol. 5771. Springer, Berlin, 163--178."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.10.004"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.5.861"},{"key":"e_1_2_1_15_1","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting M.","unstructured":"M. Fitting . 1983. Proof Methods for Modal and Intuitionistic Logics . Synthese Library, Vol . 169. D. Reidel Publishing Co. , Dordrecht, The Netherlands. M. Fitting. 1983. Proof Methods for Modal and Intuitionistic Logics. Synthese Library, Vol. 169. D. Reidel Publishing Co., Dordrecht, The Netherlands."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00048-6"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.669"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.3.451"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"R. Gor\u00e9 L. Postniece and A. Tiu. 2011. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science 7 2 2:8 38.  R. Gor\u00e9 L. Postniece and A. Tiu. 2011. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science 7 2 2:8 38.","DOI":"10.2168\/LMCS-7(2:8)2011"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182614"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"G. E. Hughes and M. J. Cresswell. 1996. A New Introduction to Modal Logic. Routledge London.  G. E. Hughes and M. J. Cresswell. 1996. A New Introduction to Modal Logic. Routledge London.","DOI":"10.4324\/9780203290644"},{"key":"#cr-split#-e_1_2_1_23_1.1","doi-asserted-by":"crossref","unstructured":"E. Je\u0159\u00e1bek. 2015. A note on the substructural hierarchy. Mathematical Logic Quarterly. DOI:10.1002\/malq.201500066 10.1002\/malq.201500066","DOI":"10.1002\/malq.201500066"},{"key":"#cr-split#-e_1_2_1_23_1.2","doi-asserted-by":"crossref","unstructured":"E. Je\u0159\u00e1bek. 2015. A note on the substructural hierarchy. Mathematical Logic Quarterly. DOI:10.1002\/malq.201500066","DOI":"10.1002\/malq.201500066"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053026"},{"key":"e_1_2_1_25_1","volume-title":"Proof Theory of Modal Logic (Hamburg","author":"Kracht M.","year":"1993","unstructured":"M. Kracht . 1996. Power and weakness of the modal display calculus . In Proof Theory of Modal Logic (Hamburg , 1993 ). Applied Logic Series, Vol . 2. Kluwer Academic Publishers , Dordrecht, The Netherlands, 93--121. M. Kracht. 1996. Power and weakness of the modal display calculus. In Proof Theory of Modal Logic (Hamburg, 1993). Applied Logic Series, Vol. 2. Kluwer Academic Publishers, Dordrecht, The Netherlands, 93--121."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.47"},{"key":"e_1_2_1_27_1","volume-title":"From categorical grammar to bilinear logic","author":"Lambek J.","unstructured":"J. Lambek . 1993. From categorical grammar to bilinear logic . In Substructural Logics, K. Dosen and P. Schrieder-Heister (Eds.). Oxford University Press , New York, NY , 207--237. J. Lambek. 1993. From categorical grammar to bilinear logic. In Substructural Logics, K. Dosen and P. Schrieder-Heister (Eds.). Oxford University Press, New York, NY, 207--237."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_23"},{"key":"e_1_2_1_29_1","volume-title":"Lecture Notes in Computer Science","volume":"8123","author":"Lellmann B.","unstructured":"B. Lellmann and D. Pattinson . 2013. Correspondence between modal Hilbert axioms and sequent rules with an application to S5. In Tableaux 2013 . Lecture Notes in Computer Science , Vol. 8123 . Springer, Berlin, 219--233. B. Lellmann and D. Pattinson. 2013. Correspondence between modal Hilbert axioms and sequent rules with an application to S5. In Tableaux 2013. Lecture Notes in Computer Science, Vol. 8123. Springer, Berlin, 219--233."},{"key":"e_1_2_1_30_1","unstructured":"S. Marin and L. Stra\u00dfburger. 2014. Label-free modular systems for classical and intuitionistic modal logics. In Advances in Modal Logic. Volume 10. College Publications London 387--406.  S. Marin and L. Stra\u00dfburger. 2014. Label-free modular systems for classical and intuitionistic modal logics. In Advances in Modal Logic. Volume 10. College Publications London 387--406."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu061"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1017998605966"},{"key":"e_1_2_1_35_1","volume-title":"Displaying Modal Logic. Trends in Logic","author":"Wansing H.","unstructured":"H. Wansing . 1998. Displaying Modal Logic. Trends in Logic . Springer . H. Wansing. 1998. Displaying Modal Logic. Trends in Logic. Springer."},{"key":"e_1_2_1_36_1","volume-title":"Handbook of Philosophical Logic","author":"Wansing H.","unstructured":"H. Wansing . 2002. Sequent systems for modal logics . In Handbook of Philosophical Logic , D. Gabbay and F. Guenthner (Eds.). Vol. 8 . Kluwer , 61--145. H. Wansing. 2002. Sequent systems for modal logics. In Handbook of Philosophical Logic, D. Gabbay and F. Guenthner (Eds.). Vol. 8. Kluwer, 61--145."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.3166\/jancl.18.341-364"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004218110879"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2874775","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2874775","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:54Z","timestamp":1750225734000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2874775"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,17]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,7,22]]}},"alternative-id":["10.1145\/2874775"],"URL":"https:\/\/doi.org\/10.1145\/2874775","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,17]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-02-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}