{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T01:57:27Z","timestamp":1777687047802,"version":"3.51.4"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,4,2]],"date-time":"2018-04-02T00:00:00Z","timestamp":1522627200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FWF","award":["W1255-N23 and START Y544-N23"],"award-info":[{"award-number":["W1255-N23 and START Y544-N23"]}]},{"DOI":"10.13039\/501100001821","name":"WWTF","doi-asserted-by":"crossref","award":["MA16-028"],"award-info":[{"award-number":["MA16-028"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,4,30]]},"abstract":"<jats:p>We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.<\/jats:p>","DOI":"10.1145\/3180075","type":"journal-article","created":{"date-parts":[[2018,4,2]],"date-time":"2018-04-02T12:12:24Z","timestamp":1522671144000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Hypersequents and Systems of Rules"],"prefix":"10.1145","volume":"19","author":[{"given":"Agata","family":"Ciabattoni","sequence":"first","affiliation":[{"name":"TU Wien"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco A.","family":"Genco","sequence":"additional","affiliation":[{"name":"TU Wien"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,4,2]]},"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","volume-title":"Genco","author":"Aschieri Federico","year":"2017","unstructured":"Federico Aschieri , Agata Ciabattoni , and Francesco A . Genco . 2017 . G\u00f6del logic: From natural deduction to parallel computation. In Proceedings of LICS\u201917. IEEE Computer Society . Federico Aschieri, Agata Ciabattoni, and Francesco A. Genco. 2017. G\u00f6del logic: From natural deduction to parallel computation. In Proceedings of LICS\u201917. IEEE Computer Society."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273828"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"e_1_2_1_5_1","volume-title":"The method of hypersequents in the proof theory of propositional non-classical logics","author":"Avron Arnon","year":"1993","unstructured":"Arnon Avron . 1996. The method of hypersequents in the proof theory of propositional non-classical logics . In Logic : From Foundations to Applications (Staffordshire, 1993 ). Oxford University Press , New York, 1--32. Arnon Avron. 1996. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From Foundations to Applications (Staffordshire, 1993). Oxford University Press, New York, 1--32."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Matthias Baaz Agata Ciabattoni and Christian Ferm\u00fcller. 2000. A natural deduction system for intuitionistic fuzzy logic. In Lectures on Soft Computing and Fuzzy Logic. 1--18.  Matthias Baaz Agata Ciabattoni and Christian Ferm\u00fcller. 2000. A natural deduction system for intuitionistic fuzzy logic. In Lectures on Soft Computing and Fuzzy Logic. 1--18.","DOI":"10.1007\/978-3-7908-1818-5_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.57"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.39"},{"key":"e_1_2_1_9_1","volume-title":"Genco","author":"Ciabattoni Agata","year":"2016","unstructured":"Agata Ciabattoni and Francesco A . Genco . 2016 . Embedding formalisms: Hypersequents and two-level systems of rules. In Advances in Modal Logic. Vol. 11 . College Publications , 197--216. Agata Ciabattoni and Francesco A. Genco. 2016. Embedding formalisms: Hypersequents and two-level systems of rules. In Advances in Modal Logic. Vol. 11. College Publications, 197--216."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647850.737233"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.004"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_13_1","volume-title":"Advances in Modal Logic","author":"Gor\u00e9 Rajeev","unstructured":"Rajeev Gor\u00e9 and Revantha Ramanayake . 2012. Labelled tree sequents, tree hypersequents, and nested (deep) sequents . In Advances in Modal Logic . College Publications , 279--299. Rajeev Gor\u00e9 and Revantha Ramanayake. 2012. Labelled tree sequents, tree hypersequents, and nested (deep) sequents. In Advances in Modal Logic. College Publications, 279--299."},{"key":"e_1_2_1_14_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"Howard William A.","unstructured":"William A. Howard . 1980. The formulae-as-types notion of construction . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism . Academic Press , 479--491. William A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 479--491."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.47"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.10.004"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273391"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-2267-3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu037"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-008-9425-4"},{"key":"e_1_2_1_21_1","volume-title":"Gentzen Calculi for Modal Propositional Logic","author":"Poggiolesi Francesca","unstructured":"Francesca Poggiolesi . 2010. Gentzen Calculi for Modal Propositional Logic . Springer . Francesca Poggiolesi. 2010. Gentzen Calculi for Modal Propositional Logic. Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu061"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_29"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-014-9562-3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/6.5.719"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3180075","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3180075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:18Z","timestamp":1750208898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3180075"}},"subtitle":["Embeddings and Applications"],"short-title":[],"issued":{"date-parts":[[2018,4,2]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4,30]]}},"alternative-id":["10.1145\/3180075"],"URL":"https:\/\/doi.org\/10.1145\/3180075","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,2]]},"assertion":[{"value":"2017-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-04-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}