{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:30:24Z","timestamp":1740123024269,"version":"3.37.3"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,3,26]],"date-time":"2021-03-26T00:00:00Z","timestamp":1616716800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,3,26]],"date-time":"2021-03-26T00:00:00Z","timestamp":1616716800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Horizon 2020 research and innovation program","award":["689176"],"award-info":[{"award-number":["689176"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s11225-021-09941-6","type":"journal-article","created":{"date-parts":[[2021,3,26]],"date-time":"2021-03-26T12:02:51Z","timestamp":1616760171000},"page":"1119-1157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Hyper-MacNeille Completions of Heyting Algebras"],"prefix":"10.1007","volume":"109","author":[{"given":"J.","family":"Harding","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9131-9134","authenticated-orcid":false,"given":"F. M.","family":"Lauridsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,26]]},"reference":[{"key":"9941_CR1","volume-title":"Distributive Lattices, University of Missouri Press","author":"R Balbes","year":"1974","unstructured":"Balbes, R., and Ph. Dwinger, Distributive Lattices, University of Missouri Press, Columbia, Mo., 1974."},{"issue":"2","key":"9941_CR2","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1023\/B:STUD.0000037127.15182.2a","volume":"77","author":"F Belardinelli","year":"2004","unstructured":"Belardinelli, F., P. Jipsen, and H. Ono, Algebraic aspects of cut elimination, Studia Logica 77(2):209\u2013240, 2004.","journal-title":"Studia Logica"},{"key":"9941_CR3","doi-asserted-by":"crossref","unstructured":"Bezhanishvili, G., J. Harding, J. Ilin, and F.\u00a0M. Lauridsen, MacNeille transferability and stable classes of Heyting algebras, Algebra Universalis 79:55, 2018.","DOI":"10.1007\/s00012-018-0534-8"},{"key":"9941_CR4","unstructured":"Bezhanishvili, N., Lattices of Intermediate and Cylindric Modal Logics, Ph.D.\u00a0Thesis, University of Amsterdam, 2006."},{"key":"9941_CR5","doi-asserted-by":"crossref","unstructured":"Blackburn, P., M. de\u00a0Rijke, and Y. Venema, Modal Logic, vol.\u00a053 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"9941_CR6","doi-asserted-by":"crossref","unstructured":"Burris, S., and H.\u00a0P. Sankappanavar, A Course in Universal Algebra, vol.\u00a078 of Graduate Texts in Mathematics, Springer-Verlag, New York-Berlin, 1981.","DOI":"10.1007\/978-1-4613-8130-3"},{"issue":"2","key":"9941_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1090\/S0002-9947-1979-0522263-8","volume":"248","author":"S Burris","year":"1979","unstructured":"Burris, S., and H. Werner, Sheaf constructions and their elementary properties, Transactions of the American Mathematical Society 248(2):269\u2013309, 1979.","journal-title":"Trans. Amer. Math. Soc."},{"key":"9941_CR8","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui, From axioms to analytic rules in nonclassical logics, in Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, IEEE Computer Society, 2008, pp. 229\u2013240.","DOI":"10.1109\/LICS.2008.39"},{"issue":"4","key":"9941_CR9","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/s00012-011-0160-1","volume":"66","author":"A Ciabattoni","year":"2011","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui, MacNeille completions of FL-algebras, Algebra Universalis 66(4):405\u2013420, 2011.","journal-title":"Algebra Universalis"},{"issue":"3","key":"9941_CR10","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/j.apal.2011.09.003","volume":"163","author":"A Ciabattoni","year":"2012","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui, Algebraic proof theory for substructural logics: cut-elimination and completions, Annals of Pure and Applied Logic 163(3):266\u2013290, 2012.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"9941_CR11","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1016\/j.apal.2016.10.012","volume":"168","author":"A Ciabattoni","year":"2017","unstructured":"Ciabattoni, A., N. Galatos, and K. Terui, Algebraic proof theory: hypersequents and hypercompletions, Annals of Pure and Applied Logic 168(3): 693\u2013737, 2017.","journal-title":"Annals of Pure and Applied Logic"},{"key":"9941_CR12","doi-asserted-by":"crossref","unstructured":"Ciabattoni, A., P. Maffezioli, and L. Spendier, Hypersequent and labelled calculi for intermediate logics, in Automated Reasoning with Analytic Tableaux and Related Methods, vol. 8123 of Lecture Notes in Comput. Sci., Springer, Heidelberg, 2013, pp. 81\u201396.","DOI":"10.1007\/978-3-642-40537-2_9"},{"key":"9941_CR13","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2140\/pjm.1971.38.29","volume":"38","author":"SD Comer","year":"1971","unstructured":"Comer, S.\u00a0D., Pacific Journal of Mathematics 38: Representations by algebras of sections over Boolean spaces, 29\u201338, 1971.","journal-title":"Pacific J. Math."},{"key":"9941_CR14","doi-asserted-by":"crossref","unstructured":"Conradie, W., S. Ghilardi, and A. Palmigiano, Unified correspondence, in Johan van Benthem on Logic and Information Dynamics, vol.\u00a05 of Outst. Contrib. Log., Springer, Cham, 2014, pp. 933\u2013975.","DOI":"10.1007\/978-3-319-06025-5_36"},{"issue":"3","key":"9941_CR15","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/j.apal.2011.10.004","volume":"163","author":"W Conradie","year":"2012","unstructured":"Conradie, W., and A. Palmigiano, Algorithmic correspondence and canonicity for distributive modal logic, Annals of Pure and Applied Logic 163(3):338\u2013376, 2012.","journal-title":"Ann. Pure Appl. Logic"},{"key":"9941_CR16","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlamp.2016.10.006","volume":"91","author":"W Conradie","year":"2017","unstructured":"Conradie, W., A. Palmigiano, and S. Sourabh, Algebraic modal correspondence: Sahlqvist and beyond, Journal of Logical and Algebraic Methods in Programming 91:60\u201384, 2017.","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"2","key":"9941_CR17","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF00389840","volume":"13","author":"GD Crown","year":"1996","unstructured":"Crown, G.\u00a0D., J. Harding, and M.\u00a0F. Janowitz, Boolean products of lattices, Order 13(2):175\u2013205, 1996.","journal-title":"Order"},{"key":"9941_CR18","doi-asserted-by":"crossref","unstructured":"Davey, B.\u00a0A., $${\\mathfrak{M}}$$-Stone lattices, Canadian Journal of Mathematics 24:1027\u20131032, 1972.","DOI":"10.4153\/CJM-1972-104-x"},{"key":"9941_CR19","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF01214692","volume":"134","author":"BA Davey","year":"1973","unstructured":"Davey, B.\u00a0A., Sheaf spaces and sheaves of universal algebras, Mathematische Zeitschrift 134:275\u2013290, 1973.","journal-title":"Math. Z."},{"key":"9941_CR20","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"2002","unstructured":"Davey, B.\u00a0A., and H.\u00a0A. Priestley, Introduction to Lattices and Order, second edn., Cambridge University Press, New York, 2002.","edition":"2"},{"key":"9941_CR21","first-page":"111","volume-title":"\u2018The Dedekind completion of $$C(X)$$ with pointwise discontinuous functions\u2019, in Ordered Structures and Applications","author":"N D\u0103ne\u0163","year":"2016","unstructured":"D\u0103ne\u0163, N., The Dedekind completion of $$C(X)$$ with pointwise discontinuous functions, in Ordered Structures and Applications, Trends Math., Birkh\u00e4user\/Springer, Cham, 2016, pp. 111\u2013126."},{"key":"9941_CR22","unstructured":"Esakia, L., Heyting Algebras I. Duality Theory, \u201cMetsniereba\u201d, Tbilisi, 1985. (Russian)."},{"key":"9941_CR23","doi-asserted-by":"crossref","unstructured":"Esakia, L., Heyting Algebras: Duality Theory, vol.\u00a050 of Trends in Logic, Springer, 2019. Translated from the Russian by A.\u00a0Evseev.","DOI":"10.1007\/978-3-030-12096-2"},{"issue":"3","key":"9941_CR24","doi-asserted-by":"publisher","first-page":"1219","DOI":"10.1090\/S0002-9947-2012-05573-5","volume":"365","author":"N Galatos","year":"2013","unstructured":"Galatos, N., and P. Jipsen, Residuated frames with applications to decidability, Transactions of the American Mathematical Society 365(3):1219\u20131249, 2013.","journal-title":"Trans. Amer. Math. Soc."},{"issue":"9","key":"9941_CR25","doi-asserted-by":"publisher","first-page":"1097","DOI":"10.1016\/j.apal.2010.01.003","volume":"161","author":"N Galatos","year":"2010","unstructured":"Galatos, N., and H. Ono, Cut elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic 161(9):1097\u20131133, 2010.","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"9941_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1002\/malq.19910370103","volume":"37","author":"M Gehrke","year":"1991","unstructured":"Gehrke, M., The order structure of Stone spaces and the $$T_D$$-separation axiom, Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik 37(1):5\u201315, 1991.","journal-title":"Z. Math. Logik Grundlag. Math."},{"issue":"1","key":"9941_CR27","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/jabr.2000.8622","volume":"238","author":"M Gehrke","year":"2001","unstructured":"Gehrke, M., and J. Harding, Bounded lattice expansions, Journal of Algebra 238(1):345\u2013371, 2001.","journal-title":"J. Algebra"},{"issue":"2","key":"9941_CR28","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1090\/S0002-9947-05-03816-X","volume":"358","author":"M Gehrke","year":"2006","unstructured":"Gehrke, M., J. Harding, and Y. Venema, MacNeille completions and canonical extensions, Transactions of the American Mathematical Society 358(2):573\u2013590, 2006.","journal-title":"Trans. Amer. Math. Soc."},{"issue":"8","key":"9941_CR29","doi-asserted-by":"publisher","first-page":"2164","DOI":"10.1016\/j.jpaa.2017.09.004","volume":"222","author":"M Gehrke","year":"2018","unstructured":"Gehrke, M., and S.\u00a0J. van Gool, Sheaves and duality, Journal of Pure and Applied Algebra 222(8):2164\u20132180, 2018.","journal-title":"J. Pure Appl. Algebra"},{"issue":"1","key":"9941_CR30","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s000120050100","volume":"41","author":"S Givant","year":"1999","unstructured":"Givant, S., and Y.\u00a0Venema, The preservation of Sahlqvist equations in completions of Boolean algebras with operators, Algebra Universalis 41(1):47\u201384, 1999.","journal-title":"Algebra Universalis"},{"key":"9941_CR31","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/BF02020328","volume":"8","author":"G Gr\u00e4tzer","year":"1957","unstructured":"Gr\u00e4tzer, G., and E.\u00a0T. Schmidt, On a problem of M.\u00a0H.\u00a0Stone, Acta Mathematica Academiae Scientiarum Hungarica 8:455\u2013460, 1957.","journal-title":"Acta Math. Acad. Sci. Hungar."},{"key":"9941_CR32","unstructured":"Greco, G., P. Jipsen, F. Liang, A. Palmigiano, and A. Tzimoulis, Algebraic proof theory for LE-logics, 2018. ArXiv:1808.04642v1."},{"issue":"2","key":"9941_CR33","first-page":"88","volume":"53","author":"G Hansoul","year":"1984","unstructured":"Hansoul, G., and L.\u00a0Vrancken-Mawet, D\u00e9compositions bool\u00e9ennes de lattis distributifs born\u00e9s, Bulletin de la Soci\u00e9t\u00e9 Royale des Sciences de Li\u00e9ge 53(2):88\u201392, 1984.","journal-title":"Bull. Soc. Roy. Sci. Li\u00e8ge"},{"issue":"3","key":"9941_CR34","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BF01110549","volume":"10","author":"J Harding","year":"1993","unstructured":"Harding, J., Completions of orthomodular lattices. II, Order 10(3):283\u2013294, 1993.","journal-title":"Order"},{"issue":"3","key":"9941_CR35","first-page":"649","volume":"34","author":"J Harding","year":"2008","unstructured":"Harding, J., A regular completion for the variety generated by the three-element Heyting algebra, Houston Journal of Mathematics 34(3):649\u2013660, 2008.","journal-title":"Houston J. Math."},{"issue":"4","key":"9941_CR36","first-page":"937","volume":"30","author":"J Harding","year":"2004","unstructured":"Harding, J., and G. Bezhanishvili, MacNeille completions of Heyting algebras, Houston Journal of Mathematics 30(4):937\u2013952, 2004.","journal-title":"Houston J. Math."},{"issue":"1967","key":"9941_CR37","first-page":"110","volume":"21","author":"B J\u00f3nsson","year":"1968","unstructured":"J\u00f3nsson, B., Algebras whose congruence lattices are distributive, Mathematica Scandinavica 21:110\u2013121, 1967.","journal-title":"Math. Scand."},{"key":"9941_CR38","unstructured":"Lauridsen, F.\u00a0M., Cuts and Completions: Algebraic aspects of structural proof theory, Ph.D.\u00a0Thesis, University of Amsterdam, 2019."},{"issue":"2","key":"9941_CR39","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s11225-018-9791-y","volume":"107","author":"FM Lauridsen","year":"2019","unstructured":"Lauridsen, F.\u00a0M., Intermediate logics admitting a structural hypersequent calculus, Studia Logica 107(2):247\u2013282, 2019.","journal-title":"Studia Logica"},{"issue":"2","key":"9941_CR40","doi-asserted-by":"publisher","first-page":"509","DOI":"10.21099\/tkbjm\/1496161672","volume":"15","author":"S Maehara","year":"1991","unstructured":"Maehara, S., Lattice-valued representation of the cut-elimination theorem, Tsukuba Journal of Mathematics 15(2):509\u2013521, 1991.","journal-title":"Tsukuba J. Math."},{"key":"9941_CR41","doi-asserted-by":"crossref","unstructured":"Okada, M., Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic, Theoretical Computer Science 227(1-2):333\u2013396, 1999.","DOI":"10.1016\/S0304-3975(99)00058-4"},{"issue":"1\u20132","key":"9941_CR42","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1016\/S0304-3975(02)00024-5","volume":"281","author":"M Okada","year":"2002","unstructured":"Okada, M., A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science 281(1-2):471\u2013498, 2002.","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"9941_CR43","doi-asserted-by":"publisher","first-page":"790","DOI":"10.2307\/2586501","volume":"64","author":"M Okada","year":"1999","unstructured":"Okada, M., and K. Terui, The finite model property for various fragments of intuitionistic linear logic, Journal of Symbolic Logic 64(2):790\u2013802, 1999.","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"9941_CR44","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1023\/A:1025171301247","volume":"74","author":"H Ono","year":"2003","unstructured":"Ono, H., Closure operators and complete embeddings of residuated lattices, Studia Logica 74(3):427\u2013440, 2003.","journal-title":"Studia Logica"},{"issue":"1","key":"9941_CR45","doi-asserted-by":"publisher","first-page":"169","DOI":"10.2307\/2273798","volume":"50","author":"H Ono","year":"1985","unstructured":"Ono, H., and Y. Komori, Logics without the contraction rule, Journal of Symbolic Logic 50(1):169\u2013201, 1985.","journal-title":"J. Symbolic Logic"},{"key":"9941_CR46","doi-asserted-by":"crossref","unstructured":"Pierce, R.\u00a0S., Modules over Commutative Regular Rings, Memoirs of the American Mathematical Society, No. 70, Amer. Math. Soc., Providence, R.I., 1967.","DOI":"10.1090\/memo\/0070"},{"key":"9941_CR47","doi-asserted-by":"crossref","unstructured":"Priestley, H.\u00a0A., Ordered topological spaces and the representation of distributive lattices, Proceedings of the London Mathematical Society 24(3):507\u2013530, 1972.","DOI":"10.1112\/plms\/s3-24.3.507"},{"issue":"1","key":"9941_CR48","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.jpaa.2008.05.013","volume":"213","author":"W Rump","year":"2009","unstructured":"Rump, W., and Y.\u00a0C. Yang, Lateral completion and structure sheaf of an Archimedean $$l$$-group, Journal of Pure and Applied Algebra 213(1):136\u2013143, 2009.","journal-title":"J. Pure Appl. Algebra"},{"issue":"2","key":"9941_CR49","doi-asserted-by":"publisher","first-page":"405","DOI":"10.2140\/pjm.1985.117.405","volume":"117","author":"HP Sankappanavar","year":"1985","unstructured":"Sankappanavar, H.\u00a0P., Heyting algebras with dual pseudocomplementation, Pacific Journal of Mathematics 117(2):405\u2013415, 1985.","journal-title":"Pacific J. Math."},{"key":"9941_CR50","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1017\/S1446788700007205","volume":"9","author":"TP Speed","year":"1969","unstructured":"Speed, T.\u00a0P., Some remarks on a class of distributive lattices, Journal of the Australian Mathematical Society 9:289\u2013296, 1969.","journal-title":"J. Austral. Math. Soc."},{"key":"9941_CR51","first-page":"86","volume":"38","author":"TP Speed","year":"1969","unstructured":"Speed, T.\u00a0P., Two congruences on distributive lattices, Bulletin de la Soci\u00e9t\u00e9 Royale des Sciences de Li\u00e9ge 38:86\u201395, 1969.","journal-title":"Bull. Soc. Roy. Sci. Li\u00e8ge"},{"key":"9941_CR52","unstructured":"Terui, K., Herbrand\u2019s Theorem via Hypercanonical Extensions, presentation delivered on September 24 at TbiLLC 2013, Gadauri, 2013."},{"key":"9941_CR53","unstructured":"Terui, K., MacNeille completion and Buchholz\u2019 omega rule for parameter-free second order logics, in D. Ghica, and A. Jung, (eds.), 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2018, pp. 37:1\u201337:19."},{"issue":"2","key":"9941_CR54","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00012-007-2033-1","volume":"57","author":"M Theunissen","year":"2007","unstructured":"Theunissen, M., and Y. Venema, MacNeille completions of lattice expansions, Algebra Universalis 57(2):143\u2013193, 2007.","journal-title":"Algebra Universalis"},{"issue":"3","key":"9941_CR55","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF01190703","volume":"33","author":"DJ Vaggione","year":"1995","unstructured":"Vaggione, D.\u00a0J., Locally Boolean spectra, Algebra Universalis 33(3):319\u2013354, 1995.","journal-title":"Algebra Universalis"},{"issue":"4","key":"9941_CR56","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/s00012-005-1957-6","volume":"54","author":"AM Wille","year":"2005","unstructured":"Wille, A.\u00a0M., A Gentzen system for involutive residuated lattices, Algebra Universalis 54(4):449\u2013463, 2005.","journal-title":"Algebra Universalis"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09941-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-021-09941-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09941-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T14:55:36Z","timestamp":1671720936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-021-09941-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,26]]},"references-count":56,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["9941"],"URL":"https:\/\/doi.org\/10.1007\/s11225-021-09941-6","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2021,3,26]]},"assertion":[{"value":"22 January 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}