{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T14:18:24Z","timestamp":1762352304964,"version":"3.41.2"},"reference-count":53,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,7,31]],"date-time":"2012-07-31T00:00:00Z","timestamp":1343692800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/C014014\/1"],"award-info":[{"award-number":["EP\/C014014\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/H051511\/1"],"award-info":[{"award-number":["EP\/H051511\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003246","name":"Netherlands Organisation for Scientific Research","doi-asserted-by":"crossref","award":["2300130488"],"award-info":[{"award-number":["2300130488"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/F031173\/1"],"award-info":[{"award-number":["EP\/F031173\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We study the finitary version of the coalgebraic logic introduced by L. Moss.\nThe syntax of this logic, which is introduced uniformly with respect to a\ncoalgebraic type functor, required to preserve weak pullbacks, extends that of\nclassical propositional logic with a so-called coalgebraic cover modality\ndepending on the type functor. Its semantics is defined in terms of a\ncategorically defined relation lifting operation. As the main contributions of\nour paper we introduce a derivation system, and prove that it provides a sound\nand complete axiomatization for the collection of coalgebraically valid\ninequalities. Our soundness and completeness proof is algebraic, and we employ\nPattinson's stratification method, showing that our derivation system can be\nstratified in countably many layers, corresponding to the modal depth of the\nformulas involved. In the proof of our main result we identify some new\nconcepts and obtain some auxiliary results of independent interest. We survey\nproperties of the notion of relation lifting, induced by an arbitrary but fixed\nset functor. We introduce a category of Boolean algebra presentations, and\nestablish an adjunction between it and the category of Boolean algebras. Given\nthe fact that our derivation system involves only formulas of depth one, it can\nbe encoded as a endo-functor on Boolean algebras. We show that this functor is\nfinitary and preserves embeddings, and we prove that the Lindenbaum-Tarski\nalgebra of our logic can be identified with the initial algebra for this\nfunctor.<\/jats:p>","DOI":"10.2168\/lmcs-8(3:2)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T08:17:46Z","timestamp":1385713066000},"source":"Crossref","is-referenced-by-count":12,"title":["Completeness for the coalgebraic cover modality"],"prefix":"10.46298","volume":"Volume 8, Issue 3","author":[{"given":"Clemens","family":"Kupke","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Kurz","sequence":"additional","affiliation":[]},{"given":"Yde","family":"Venema","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,7,31]]},"reference":[{"key":"10.2168\/LMCS-8(3:2)2012_acze:nonw88","unstructured":"P. Aczel.Non-well-founded sets, volume 14 ofCSLI Lecture Notes. CSLI, 1988."},{"key":"10.2168\/LMCS-8(3:2)2012_acze:fina89","unstructured":"P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, A. Poign\u00e9, and D.E. Rydeheard, editors,Category Theory and Computer Science, volume 389 ofLNCS. Springer, 1989."},{"key":"10.2168\/LMCS-8(3:2)2012_adam:logi05","doi-asserted-by":"crossref","unstructured":"J. Ad\u00e1mek. A logic of coequations. In L. Ong, editor,Computer Science Logic, 19th International Workshop (CSL 2005), Proceedings, volume 3634 ofLNCS, pages 70-86. Springer, 2005.","DOI":"10.1007\/11538363_7"},{"key":"10.2168\/LMCS-8(3:2)2012_adam:grea95","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0304-3975(95)00011-K","volume":"150","author":"J. Ad\u00e1mek and V. Koubek","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_cmcs4","doi-asserted-by":"crossref","unstructured":"J. Ad\u00e1mek and S. Milius, editors.Coalgebraic Methods in Computer Science (CMCS'04), volume 106 ofENTCS, 2004. J. Ad\u00e1mek and J. Rosick\u00fd.Locally Presentable and Accessible Categories, volume 189 ofLMS Lecture Note Series. Cambridge University Press, 1994.","DOI":"10.1017\/CBO9780511600579"},{"key":"10.2168\/LMCS-8(3:2)2012_adam:auto90","unstructured":"J. Ad\u00e1mek and V. Trnkov\u00e1.Automata and Algebras in Categories. Kluwer Academic Publishers, 1990."},{"key":"10.2168\/LMCS-8(3:2)2012_DBLP:conf\/aiml\/2008","unstructured":"C. Areces and R. Goldblatt, editors.Advances in Modal Logic 7. College Publications, 2008. A. Baltag. A logic for coalgebraic simulation. In Reichel cmcs0, pages 41-60."},{"key":"10.2168\/LMCS-8(3:2)2012_barr:rela70","doi-asserted-by":"crossref","unstructured":"M. Barr. Relational algebras. InReports of the Midwest Category Seminar IV, volume 137 ofLecture Notes in Mathematics, pages 39-55, 1970.","DOI":"10.1007\/BFb0060439"},{"key":"10.2168\/LMCS-8(3:2)2012_beck:dist69","doi-asserted-by":"crossref","unstructured":"J. Beck. Distributive Laws. InSeminar on Triples and Categorical Homology Theory, volume 80 ofLecture Notes in Mathematics, pages 119-140. Springer, 1969.","DOI":"10.1007\/BFb0083084"},{"key":"10.2168\/LMCS-8(3:2)2012_berg:moss09","unstructured":"J. Bergfeld. Moss's coalgebraic logic: Examples and completeness results. Master's thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2009."},{"key":"10.2168\/LMCS-8(3:2)2012_bilk:proo08","unstructured":"M. B\u00edlkov\u00e1, A. Palmigiano, and Y. Venema. Proof systems for the coalgebraic cover modality. In Areces and Goldblatt DBLP:conf\/aiml\/2008, pages 1-21."},{"key":"10.2168\/LMCS-8(3:2)2012_bilk:proo10","unstructured":"M. B\u00edlkov\u00e1, A. Palmigiano, and Y. Venema. Proof systems for Moss' coalgebraic logic. In preparation, 2010."},{"key":"10.2168\/LMCS-8(3:2)2012_bilk:monoxx","unstructured":"M. B\u00edlkov\u00e1, J. Velebil, and Y. Venema. On monotone modalities and adjointness.Mathematical Structures in Computer Science, to appear."},{"key":"10.2168\/LMCS-8(3:2)2012_blac:moda01","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. de Rijke, and Y. Venema.Modal Logic. Number 53 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"10.2168\/LMCS-8(3:2)2012_bons:dual05","doi-asserted-by":"crossref","unstructured":"M. Bonsangue and A. Kurz. Duality for logics of transition systems. In V. Sassone, editor,Foundations of Software Science and Computational Structures, 8th International Conference (FoSSaCS'05), volume 3441 ofLNCS, pages 455-469. Springer, 2005.","DOI":"10.1007\/978-3-540-31982-5_29"},{"issue":"4","key":"10.2168\/LMCS-8(3:2)2012_carb:2cat91","first-page":"47","volume":"31","author":"A. Carboni, G. Kelly, and R. Wood","year":"1991","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"10.2168\/LMCS-8(3:2)2012_cirstea:cmcs04","doi-asserted-by":"crossref","unstructured":"C. Cirstea. On logics for coalgebraic simulation. In Ad\u00e1mek and Milius cmcs4, pages 63-90.","DOI":"10.1016\/j.entcs.2004.02.026"},{"key":"10.2168\/LMCS-8(3:2)2012_dago:logi00","doi-asserted-by":"crossref","first-page":"310","DOI":"10.2307\/2586539","volume":"65","author":"G. D'Agostino and M. Hollenberg","year":"2000","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(3:2)2012_fine:norm75","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1305\/ndjfl\/1093891703","volume":"16","author":"K. Fine","year":"1975","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"2-3","key":"10.2168\/LMCS-8(3:2)2012_gumm01:func","first-page":"135","volume":"45","author":"H.P. Gumm","year":"2001","journal-title":"Algebra Universalis"},{"key":"10.2168\/LMCS-8(3:2)2012_gumm05:from","doi-asserted-by":"crossref","unstructured":"H.P. Gumm. From T-coalgebras to filter structures and transition systems. In J. L. Fiadeiro, editor,Algebra and Coalgebra in Computer Science (CALCO 2005), volume 3629 ofLNCS, pages 194-212, 2005.","DOI":"10.1007\/11548133_13"},{"issue":"12","key":"10.2168\/LMCS-8(3:2)2012_hermida:relational-modalities","doi-asserted-by":"crossref","first-page":"1505","DOI":"10.1016\/j.ic.2010.09.009","volume":"209","author":"C. Hermida","year":"2011","journal-title":"Inf. Comput."},{"issue":"2","key":"10.2168\/LMCS-8(3:2)2012_herm98:stru","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1006\/inco.1998.2725","volume":"145","author":"C. Hermida and B. Jacobs","year":"1998","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(3:2)2012_hodg:mode93","doi-asserted-by":"crossref","unstructured":"W. Hodges.Model Theory. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511551574"},{"key":"10.2168\/LMCS-8(3:2)2012_hugh-jaco:simulations","doi-asserted-by":"crossref","unstructured":"J. Hughes and B. Jacobs. Simulations in coalgebra.Theoretical Computer Science, 327, 2004.","DOI":"10.1016\/j.tcs.2004.07.022"},{"issue":"1","key":"10.2168\/LMCS-8(3:2)2012_jaco:many01","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1051\/ita:2001108","volume":"35","author":"B. Jacobs","year":"2001","journal-title":"Theoretical Informatics and Applications"},{"key":"10.2168\/LMCS-8(3:2)2012_bart04:trac","doi-asserted-by":"crossref","unstructured":"B. Jacobs. Trace semantics for coalgebras. In Ad\u00e1mek and Milius cmcs4, pages 167-184.","DOI":"10.1016\/j.entcs.2004.02.031"},{"key":"10.2168\/LMCS-8(3:2)2012_jani:auto95","doi-asserted-by":"crossref","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal\u00ce\u00bc-calculus and related results. In J. Wiedermann and P. H\u00e1jek, editors,Mathematical Foundations of Computer Science 1995, 20th International Symposium (MFCS'95), volume 969 ofLNCS, pages 552-562. Springer, 1995.","DOI":"10.1007\/3-540-60246-1_160"},{"key":"10.2168\/LMCS-8(3:2)2012_kiss:comp09","doi-asserted-by":"crossref","unstructured":"C. Kissig and Y. Venema. Complementation of coalgebra automata. In Kurz et al. calco2009, pages 81-96.","DOI":"10.1007\/978-3-642-03741-2_7"},{"key":"10.2168\/LMCS-8(3:2)2012_kupk:fini06","unstructured":"C. Kupke.Finitary coalgebraic logics. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2006."},{"key":"10.2168\/LMCS-8(3:2)2012_kupk:ston04","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.tcs.2004.07.023","volume":"327","author":"C. Kupke, A. Kurz, and Y. Venema","year":"2004","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_kupk:comp08","unstructured":"C. Kupke, A. Kurz, and Y. Venema. Completeness of the finitary Moss logic. In Areces and Goldblatt DBLP:conf\/aiml\/2008, pages 193-217."},{"key":"10.2168\/LMCS-8(3:2)2012_kuve08:coal","doi-asserted-by":"crossref","unstructured":"C. Kupke and Y. Venema. Coalgebraic automata theory: Basic results.Logical Methods in Computer Science, 4(4), 2008.","DOI":"10.2168\/LMCS-4(4:10)2008"},{"key":"10.2168\/LMCS-8(3:2)2012_kurz:cmcs98-j","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0304-3975(00)00125-0","volume":"260","author":"A. Kurz","year":"2001","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_kurz:coal06","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/1140612.1140628","volume":"37","author":"A. Kurz","year":"2006","journal-title":"SIGACT News"},{"key":"10.2168\/LMCS-8(3:2)2012_kurz:modaxx","unstructured":"A. Kurz and R. Leal. Modalities in the stone age: a comparison of coalgebraic logics.Theoretical Computer Science, to appear."},{"key":"10.2168\/LMCS-8(3:2)2012_calco2009","doi-asserted-by":"crossref","unstructured":"A. Kurz, M. Lenisa, and A. Tarlecki, editors.Algebra and Coalgebra in Computer Science (CALCO 2009), volume 5728 ofLNCS, 2009. S. Mac Lane.Categories for the working mathematician, volume 2 ofGraduate Texts in Mathematics. Springer, 1998.","DOI":"10.1007\/978-3-642-03741-2"},{"key":"10.2168\/LMCS-8(3:2)2012_moss:coal99","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/S0168-0072(98)00042-6","volume":"96","author":"L. Moss","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(3:2)2012_palm:nabl07","doi-asserted-by":"crossref","unstructured":"A. Palmigiano and Y. Venema. Nabla algebras and Chu spaces. In T. Mossakowski, U. Montanari, and M. Haveraaen, editors,Algebra and Coalgebra in Computer Science (CALCO 2007), volume 4624 ofLNCS, pages 394-408, 2007.","DOI":"10.1007\/978-3-540-73859-6_27"},{"issue":"1-3","key":"10.2168\/LMCS-8(3:2)2012_patt:coal03","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0304-3975(03)00201-9","volume":"309","author":"D. Pattinson","year":"2003","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_cmcs0","unstructured":"H. Reichel, editor.Coalgebraic Methods in Computer Science (CMCS'00), volume 33 ofENTCS, 2000. M. R\u00f6\u00dfiger. Coalgebras and modal logic. In Reichel cmcs0, pages 299-320."},{"key":"10.2168\/LMCS-8(3:2)2012_rutt:univ00","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J. Rutten","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_sant:comp10","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/j.apal.2010.07.003","volume":"162","author":"L. Santocanale and Y. Venema","year":"2010","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-8(3:2)2012_sant:unif10","unstructured":"L. Santocanale and Y. Venema. Uniform interpolation for monotone modal logic. In L. Beklemishev, V. Goranko, and V. Shehtman, editors,Advances in Modal Logic 8. College Publications, 2010."},{"key":"10.2168\/LMCS-8(3:2)2012_schr:expr05","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1016\/j.tcs.2007.09.023","volume":"390","author":"Lutz Schr\u00f6der","year":"2008","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(3:2)2012_siko:theo48","unstructured":"R. Sikorski. A theorem on extensions of homomorphisms.Annals of the Polish Mathematical Society, 21, 1948."},{"key":"10.2168\/LMCS-8(3:2)2012_staton:calco09","doi-asserted-by":"crossref","unstructured":"S. Staton. Relating coalgebraic notions of bisimulation with applications to name-passing process calculi. In Kurz et al. calco2009, pages 191-205.","DOI":"10.1007\/978-3-642-03741-2_14"},{"issue":"2","key":"10.2168\/LMCS-8(3:2)2012_Street:Monads","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0022-4049(72)90019-9","volume":"2","author":"R. Street","year":"1972","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.2168\/LMCS-8(3:2)2012_thijs:diss","unstructured":"A. Thijs.Simulation and Fixpoint Semantics. PhD thesis, Rijksuniversiteit Groningen, 1996."},{"issue":"2","key":"10.2168\/LMCS-8(3:2)2012_trnk80:gene","doi-asserted-by":"crossref","first-page":"189","DOI":"10.3233\/FI-1980-3208","volume":"3","author":"V. Trnkov\u00e1","year":"1980","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-8(3:2)2012_vene:auto06","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1016\/j.ic.2005.06.003","volume":"204","author":"Y. Venema","year":"2006","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(3:2)2012_vene:powe10","unstructured":"Y. Venema, S. Vickers, and J. Vosmaer. Powerlocales via relation lifting. In preparation, 2010."},{"key":"10.2168\/LMCS-8(3:2)2012_walu:comp00","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1999.2836","volume":"157","author":"I. Walukiewicz","year":"2000","journal-title":"Information and Computation"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/896\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/896\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:58:51Z","timestamp":1681243131000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/896"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,31]]},"references-count":53,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(3:2)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1206.4935","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1206.4935","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,7,31]]},"article-number":"896"}}