{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T11:40:05Z","timestamp":1718970005518},"reference-count":47,"publisher":"Oxford University Press (OUP)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"DOI":"10.1093\/logcom\/exw029","type":"journal-article","created":{"date-parts":[[2016,12,23]],"date-time":"2016-12-23T15:56:37Z","timestamp":1482508597000},"page":"exw029","source":"Crossref","is-referenced-by-count":0,"title":["One-step Heyting Algebras and Hypersequent Calculi with the Bounded Proof Property"],"prefix":"10.1093","author":[{"given":"Nick","family":"Bezhanishvili","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"Frederik M\u00f6llerstr\u00f6m","family":"Lauridsen","sequence":"additional","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2016,12,22]]},"reference":[{"key":"2016122217402794000_exw029v1.1","first-page":"1","article-title":"A Cook's tour of the finitary non-well-founded sets","volume-title":"We Will Show Them! Essays in Honour of Dov Gabbay","volume":"1","author":"Abramsky","year":"2005"},{"key":"2016122217402794000_exw029v1.2","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/BF01448035","article-title":"Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik","volume":"110","author":"Ackermann","year":"1935","journal-title":"Math. Ann."},{"key":"2016122217402794000_exw029v1.3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/j.apal.2008.04.003","article-title":"G\u00f6del algebras free over finite distributive lattices","volume":"155","author":"Aguzzoli","year":"2008","journal-title":"Annuals of Pure and Applied Logic"},{"key":"2016122217402794000_exw029v1.4","doi-asserted-by":"publisher","DOI":"10.2307\/2273828"},{"key":"2016122217402794000_exw029v1.5","doi-asserted-by":"crossref","unstructured":"Avron A. Hodges W. The method of hypersequents in the proof theory of propositional non-classical logics. In Logic: From Foundations to Applications, pp. 1\u201332. Oxford University Press, 1996.","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"2016122217402794000_exw029v1.6","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1017\/S0960129509990302","article-title":"Bitopological duality for distributive lattices and Heyting algebras","volume":"20","author":"Bezhanishvili","year":"2010","journal-title":"Mathematics Structures Computer Science"},{"key":"2016122217402794000_exw029v1.7","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1017\/jsl.2015.54","article-title":"Stable canonical rules","volume":"81","author":"Bezhanishvili","year":"2016","journal-title":"Journal of Symbolic Logic"},{"key":"2016122217402794000_exw029v1.8","doi-asserted-by":"crossref","unstructured":"Bezhanishvili G. Bezhanishvili N. Ilin J. Cofinal stable logics. Studia Logica, 2016. Forthcoming. doi:10.1007\/s11225-016-9677-9.","DOI":"10.1007\/s11225-016-9677-9"},{"key":"2016122217402794000_exw029v1.9","unstructured":"Bezhanishvili G. Bezhanishvili N. Locally finite reducts of Heyting algebras and canonical formulas. Notre Dame J. of Formal Logic. Forthcoming. Available as Utrecht University Logic Group Preprint Series Report 2013-305."},{"key":"2016122217402794000_exw029v1.10","doi-asserted-by":"crossref","unstructured":"Bezhanishvili N. de Jongh D. Stable formulas in intuitionistic logic. Notre Dame Journal of Formal Logic. Forthcoming. Available as ILLC Prepublication Series Report PP-2014-19.","DOI":"10.1215\/00294527-2017-0030"},{"key":"2016122217402794000_exw029v1.11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-7(2:9)2011","article-title":"Finitely generated free Heyting algebras via Birkhoff duality and coalgebra","volume":"7","author":"Bezhanishvili","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"2016122217402794000_exw029v1.12","doi-asserted-by":"crossref","unstructured":"Bezhanishvili N. Ghilardi S. Jibladze M. Bezhanishvili G. Free modal algebras revisited: the step-by-step method. In Leo Esakia on Duality in Modal and Intuitionistic Logics, pp. 43\u201362. Trends in Logic, 2014.","DOI":"10.1007\/978-94-017-8860-1_3"},{"key":"2016122217402794000_exw029v1.13","doi-asserted-by":"crossref","first-page":"1832","DOI":"10.1016\/j.apal.2014.07.005","article-title":"The bounded proof property via step algebras and step frames","volume":"165","author":"Bezhanishvili","year":"2014","journal-title":"Annuals of Pure Applied Logic"},{"key":"2016122217402794000_exw029v1.14","unstructured":"Bezhanishvili N. Ghilardi S. Multiple-conclusion rules, hypersequents syntax and step frames. In Gor\u00e9 et al. [36], pp. 54\u201373."},{"key":"2016122217402794000_exw029v1.15","doi-asserted-by":"crossref","unstructured":"Bezhanishvili N. Kurz A. Free modal algebras: A coalgebraic perspective. In Algebra and Coalgebra in Computer Science, 2th International Conference, CALCO 2007, Proceedings, volume 4624 of Lecture Notes in Computer Science, T. Mossakowski et al., eds, pp 143\u2013157. Springer, 2007.","DOI":"10.1007\/978-3-540-73859-6_10"},{"key":"2016122217402794000_exw029v1.16","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF00247711","article-title":"Don't eliminate cut","volume":"13","author":"Boolos","year":"1984","journal-title":"J. Philosophical Logic"},{"key":"2016122217402794000_exw029v1.17","doi-asserted-by":"crossref","unstructured":"Butz C. Finitely presented Heyting algebras. Technical report, BRIC Aarhus, 1998.","DOI":"10.7146\/brics.v5i30.19436"},{"key":"2016122217402794000_exw029v1.18","doi-asserted-by":"crossref","unstructured":"Chagrov A. V. Zakharyaschev M. Modal Logic, 35 of Oxford Logic Guides. Clarendon Press, 1997.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"2016122217402794000_exw029v1.19","unstructured":"Chang C. C. Keisler H. J. Model Theory. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, Londres, 1973."},{"key":"2016122217402794000_exw029v1.20","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.2.283"},{"key":"2016122217402794000_exw029v1.21","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/s005000050047","article-title":"Cut-free proof systems for logics of weak excluded middle","volume":"2","author":"Ciabattoni","year":"1998","journal-title":"Soft Computing"},{"key":"2016122217402794000_exw029v1.22","doi-asserted-by":"crossref","unstructured":"Ciabattoni A. Galatos N. Terui K. From axioms to analytic rules in nonclassical logics. In Proceedings of the 23th Annual IEEE Symposium on Logic in Computer Science, LICS 2008, pp. 229\u2013240. IEEE Computer Society, 2008.","DOI":"10.1109\/LICS.2008.39"},{"key":"2016122217402794000_exw029v1.23","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","article-title":"Algebraic proof theory for substructural logics: Cut-elimination and completions","volume":"163","author":"Ciabattoni","year":"2012","journal-title":"Annuals of Pure Applied Logic"},{"key":"2016122217402794000_exw029v1.24","doi-asserted-by":"crossref","unstructured":"Ciabattoni A. Maffezioli P. Spendier L. Hypersequent and labelled calculi for intermediate logics. In Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013. Proceedings, volume 8123 of Lecture Notes in Computer Science, D. Galmiche et al., eds, pp. 81\u201396. Springer, 2013.","DOI":"10.1007\/978-3-642-40537-2_9"},{"key":"2016122217402794000_exw029v1.25","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.tcs.2014.10.027","article-title":"Algorithmic correspondence for intuitionistic modal mu-calculus","volume":"564","author":"Conradie","year":"2015","journal-title":"Theoretical Computer Science"},{"key":"2016122217402794000_exw029v1.26","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19890350402","article-title":"A cut-free calculus for Dummett's LC quantified","volume":"35","author":"Corsi","year":"1989","journal-title":"Zeitschr. f. math. Logik und Grundlagen d. Math."},{"key":"2016122217402794000_exw029v1.27","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs016"},{"key":"2016122217402794000_exw029v1.28","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.285"},{"key":"2016122217402794000_exw029v1.29","unstructured":"Davey B. A. Priestley H. A. Introduction to Lattices and Order. Cambridge University Press, Cambridge, 1990."},{"key":"2016122217402794000_exw029v1.30","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093891703"},{"key":"2016122217402794000_exw029v1.31","doi-asserted-by":"crossref","first-page":"911","DOI":"10.2307\/2275765","article-title":"A sheaf representation and duality for finitely presenting Heyting algebras","volume":"60","author":"Ghilardi","year":"1995","journal-title":"Journal of Symbolic Logic"},{"key":"2016122217402794000_exw029v1.32","first-page":"240","article-title":"Free Heyting algebras as bi-Heyting algebras","volume":"XIV","author":"Ghilardi","year":"1992","journal-title":"C. R. Math. Rep. Acad. Sci. Canada"},{"key":"2016122217402794000_exw029v1.33","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0168-0072(93)E0084-2","article-title":"An algebraic theory of normal forms","volume":"71","author":"Ghilardi","year":"1995","journal-title":"Annuals of Pure Applied Logic"},{"key":"2016122217402794000_exw029v1.34","doi-asserted-by":"crossref","first-page":"193","DOI":"10.3166\/jancl.20.193-217","article-title":"Continuity, freeness, and filtrations","volume":"20","author":"Ghilardi","year":"2010","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"2016122217402794000_exw029v1.35","unstructured":"van Gool S. J. Free algebras for G\u00f6del-L\u00f6b provability logic. In Gor\u00e9 et al. [36], pp. 217\u2013233."},{"key":"2016122217402794000_exw029v1.36","unstructured":"Gor\u00e9 R. , eds. Advances in Modal Logic 10. College Publications, 2014."},{"key":"2016122217402794000_exw029v1.37","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1002\/mana.19680360304","article-title":"On the existence of free structures over universal classes","volume":"36","author":"Gr\u00e4tzer","year":"1968","journal-title":"Math. Nachr."},{"key":"2016122217402794000_exw029v1.38","first-page":"89","article-title":"Cut-free hypersequent calculus for S4.3","volume":"41","author":"Indrzejczak","year":"2012","journal-title":"Bulletin of the Section of Logic"},{"key":"2016122217402794000_exw029v1.39","doi-asserted-by":"crossref","first-page":"1171","DOI":"10.2178\/jsl\/1254748686","article-title":"Canonical rules","volume":"74","author":"Je\u0159\u00e1bek","year":"2009","journal-title":"Journal of Symbolic Logic"},{"key":"2016122217402794000_exw029v1.40","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1002\/malq.201500066","article-title":"A note on the substructural hierarchy","volume":"62","author":"Je\u0159\u00e1bek","year":"2016","journal-title":"Mathematical Logic Quarterly"},{"key":"2016122217402794000_exw029v1.41","doi-asserted-by":"crossref","unstructured":"Lahav O. From frame properties to hypersequent rules in modal logics. In Proceedings of the 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 408\u2013417. IEEE Computer Society, 2013.","DOI":"10.1109\/LICS.2013.47"},{"key":"2016122217402794000_exw029v1.42","first-page":"900","article-title":"Uniform, cut-free formulations of T, S4, S5","volume":"48","author":"Pottinger","year":"1983","journal-title":"Journal of Symbolic Logic"},{"key":"2016122217402794000_exw029v1.43","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1023\/A:1015291410777","article-title":"Quasiorders and sublattices of distributive lattices","volume":"19","author":"Schmid","year":"2002","journal-title":"Order"},{"key":"2016122217402794000_exw029v1.44","doi-asserted-by":"crossref","first-page":"305","DOI":"10.2307\/2963525","article-title":"Syntactical and semantical properties of simple type theory","volume":"25","author":"Sch\u00fctte","year":"1960","journal-title":"Journal of Symbolic Logic"},{"key":"2016122217402794000_exw029v1.45","unstructured":"Sonobe O. A Gentzen-type formulation of some intermediate propositional logics. Journal of Tsuda College, 7\u201313, 1975."},{"key":"2016122217402794000_exw029v1.46","doi-asserted-by":"crossref","unstructured":"Troelstra A. S. Schwichtenberg H. Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge 2000.","DOI":"10.1017\/CBO9781139168717"},{"key":"2016122217402794000_exw029v1.47","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/BF01982017","article-title":"Syntax and semantics of superintuitionistic logics","volume":"28","author":"Zakharyaschev","year":"1989","journal-title":"Algebra and Logic"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/doi\/10.1093\/logcom\/exw029\/8520327\/exw029.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T11:18:10Z","timestamp":1718968690000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exw029"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,22]]},"references-count":47,"alternative-id":["10.1093\/logcom\/exw029"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exw029","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,22]]}}}