{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:32Z","timestamp":1762459232982},"reference-count":45,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T00:00:00Z","timestamp":1415750400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,6]]},"abstract":"<jats:p>A \u2018hybridization\u2019 of a logic, referred to as the <jats:italic>base logic<\/jats:italic>, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By \u2018hybridized institutions\u2019 we mean the result of this process when logics are treated abstractly as <jats:italic>institutions<\/jats:italic> (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000383_inline1\" \/><jats:tex-math>$\\mathcal{FOL}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>) as a \u2018hybridization\u2019 process of abstract encodings of institutions into <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000383_inline1\" \/><jats:tex-math>$\\mathcal{FOL}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, which may be seen as an abstraction of the well-known standard translation of modal logic into <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000383_inline1\" \/><jats:tex-math>$\\mathcal{FOL}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. The concept of encoding employed by our work is that of <jats:italic>comorphism<\/jats:italic> from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics\/institutions. Moreover, we consider the so-called <jats:italic>theoroidal<\/jats:italic> version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000383_inline1\" \/><jats:tex-math>$\\mathcal{FOL}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1017\/s0960129514000383","type":"journal-article","created":{"date-parts":[[2014,11,12]],"date-time":"2014-11-12T08:36:22Z","timestamp":1415781382000},"page":"745-788","source":"Crossref","is-referenced-by-count":23,"title":["Encoding hybridized institutions into first-order logic"],"prefix":"10.1017","volume":"26","author":[{"given":"R\u0102ZVAN","family":"DIACONESCU","sequence":"first","affiliation":[]},{"given":"ALEXANDRE","family":"MADEIRA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,12]]},"reference":[{"key":"S0960129514000383_ref43","first-page":"337","volume-title":"Proceedings, International Conference on Frontiers of Combining Systems","author":"Tarlecki","year":"2000"},{"key":"S0960129514000383_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61440-0_125"},{"key":"S0960129514000383_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.11.001"},{"key":"S0960129514000383_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61629-2_59"},{"key":"S0960129514000383_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45616-3_4"},{"key":"S0960129514000383_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200013"},{"key":"S0960129514000383_ref40","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzp085"},{"key":"S0960129514000383_ref29","unstructured":"Madeira A. (2013) Foundations and Techniques for Software Reconfigurability. Ph.D. thesis, Universidades do Minho, Aveiro and Porto (Joint MAP-i Doctoral Programme)"},{"key":"S0960129514000383_ref19","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exr007"},{"key":"S0960129514000383_ref27","volume-title":"A Shorter Model Theory","author":"Hodges","year":"1997"},{"key":"S0960129514000383_ref15","volume-title":"Institution-Independent Model Theory","author":"Diaconescu","year":"2008"},{"key":"S0960129514000383_ref6","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.339"},{"key":"S0960129514000383_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BF00156915"},{"key":"S0960129514000383_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0002-4"},{"key":"S0960129514000383_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17162-2_132"},{"key":"S0960129514000383_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2009.09.008"},{"key":"S0960129514000383_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.5.657"},{"key":"S0960129514000383_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.09.001"},{"key":"S0960129514000383_ref31","first-page":"275","volume-title":"Proceedings, Logic Colloquium, 1987","author":"Meseguer","year":"1989"},{"key":"S0960129514000383_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049415"},{"key":"S0960129514000383_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.02.005"},{"key":"S0960129514000383_ref21","article-title":"Quasi-varieties and initial semantics in hybridized institutions","author":"Diaconescu","year":"2013","journal-title":"Journal of Logic and Computation"},{"key":"S0960129514000383_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.068"},{"key":"S0960129514000383_ref37","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1154698588"},{"key":"S0960129514000383_ref45","doi-asserted-by":"crossref","unstructured":"Weidenbach C. , Brahm U. , Hillenbrand T. , Keen E. , Theobald C. and Topic D. (2002) Spass version 2.0. In: Proceedings of the 18th International Conference on Automated Deduction, London, UK, Springer-Verlag 275\u2013279.","DOI":"10.1007\/3-540-45620-1_22"},{"key":"S0960129514000383_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"S0960129514000383_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_28"},{"key":"S0960129514000383_ref22","first-page":"83","volume-title":"Logical Environments","author":"Diaconescu","year":"1993"},{"key":"S0960129514000383_ref4","first-page":"133","article-title":"13 questions about universal logic","volume":"35","author":"B\u00e9ziau","year":"2006","journal-title":"Bulletin of the Section of Logic"},{"key":"S0960129514000383_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"S0960129514000383_ref13","volume-title":"Analysis and Synthesis of Logics How to Cut and Paste Reasoning Systems","author":"Carnielli","year":"2008"},{"key":"S0960129514000383_ref44","volume-title":"Modal Logic and Classical Logic","author":"van Bentham","year":"1988"},{"key":"S0960129514000383_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"S0960129514000383_ref9","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/7.1.27"},{"key":"S0960129514000383_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17336-3"},{"key":"S0960129514000383_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-005-3927-y"},{"key":"S0960129514000383_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0346-0145-0"},{"key":"S0960129514000383_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000430"},{"key":"S0960129514000383_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_20"},{"key":"S0960129514000383_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90026-X"},{"key":"S0960129514000383_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00160-0"},{"key":"S0960129514000383_ref38","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"key":"S0960129514000383_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_41"},{"key":"S0960129514000383_ref28","volume-title":"Categories for the Working Mathematician","author":"Lane","year":"1998"},{"key":"S0960129514000383_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s11787-009-0005-2"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000383","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T03:05:23Z","timestamp":1555643123000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000383\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,12]]},"references-count":45,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["S0960129514000383"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000383","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,12]]}}}