{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T17:23:07Z","timestamp":1774977787576,"version":"3.50.1"},"reference-count":51,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T00:00:00Z","timestamp":1732838400000},"content-version":"am","delay-in-days":639,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DE220100544"],"award-info":[{"award-number":["DE220100544"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["20K03718"],"award-info":[{"award-number":["20K03718"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1016\/j.apal.2022.103212","type":"journal-article","created":{"date-parts":[[2022,11,23]],"date-time":"2022-11-23T14:28:11Z","timestamp":1669213691000},"page":"103212","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":3,"title":["Omitting types theorem in hybrid dynamic first-order logic with rigid symbols"],"prefix":"10.1016","volume":"174","author":[{"given":"Daniel","family":"G\u0103in\u0103","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5597-6794","authenticated-orcid":false,"given":"Guillermo","family":"Badia","sequence":"additional","affiliation":[]},{"given":"Tomasz","family":"Kowalski","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"5","key":"10.1016\/j.apal.2022.103212_br0010","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1093\/logcom\/11.5.657","article-title":"Bringing them all together","volume":"11","author":"Areces","year":"2001","journal-title":"J. Log. Comput."},{"issue":"3","key":"10.1016\/j.apal.2022.103212_br0020","doi-asserted-by":"crossref","first-page":"977","DOI":"10.2307\/2695090","article-title":"Hybrid logics: characterization, interpolation and complexity","volume":"66","author":"Areces","year":"2001","journal-title":"J. Symb. Log."},{"issue":"1\u20133","key":"10.1016\/j.apal.2022.103212_br0030","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/S0168-0072(03)00059-9","article-title":"Repairing the interpolation theorem in quantified modal logic","volume":"124","author":"Areces","year":"2003","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"10.1016\/j.apal.2022.103212_br0040","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","article-title":"CASL: the common algebraic specification language","volume":"286","author":"Astesiano","year":"2002","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.apal.2022.103212_br0050","series-title":"An Introduction to Description Logic","author":"Baader","year":"2017"},{"issue":"1\u20132","key":"10.1016\/j.apal.2022.103212_br0060","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jlap.2005.09.002","article-title":"Constructor-based observational logic","volume":"67","author":"Bidoit","year":"2006","journal-title":"J. Log. Algebraic Program."},{"issue":"3","key":"10.1016\/j.apal.2022.103212_br0070","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1093\/jigpal\/8.3.339","article-title":"Representation, reasoning, and relational structures: a hybrid logic manifesto","volume":"8","author":"Blackburn","year":"2000","journal-title":"Log. J. IGPL"},{"key":"10.1016\/j.apal.2022.103212_br0080","series-title":"Logic, Language, Information, and Computation, 26th International Workshop, Proceedings","first-page":"53","article-title":"Rigid first-order hybrid logic","volume":"vol. 11541","author":"Blackburn","year":"2019"},{"key":"10.1016\/j.apal.2022.103212_br0090","article-title":"Hybrid Logic and Its Proof-Theory","volume":"vol. 37","author":"Bra\u00fcner","year":"2011"},{"key":"10.1016\/j.apal.2022.103212_br0100","first-page":"587","article-title":"On the formula \u2018there exists x such that f(x) for all f\u2208F\u2019","volume":"11","author":"Chang","year":"1964","journal-title":"Not. Am. Math. Soc."},{"key":"10.1016\/j.apal.2022.103212_br0110","series-title":"8th Conference on Algebra and Coalgebra in Computer Science","article-title":"Hybridisation of institutions in HETS (tool paper)","volume":"vol. 139","author":"Codescu","year":"2019"},{"issue":"6","key":"10.1016\/j.apal.2022.103212_br0120","doi-asserted-by":"crossref","first-page":"1143","DOI":"10.1073\/pnas.50.6.1143","article-title":"The independence of the continuum hypothesis","volume":"50","author":"Cohen","year":"1963","journal-title":"Proc. Natl. Acad. Sci. USA"},{"issue":"1","key":"10.1016\/j.apal.2022.103212_br0130","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1073\/pnas.51.1.105","article-title":"The independence of the continuum hypothesis, II","volume":"51","author":"Cohen","year":"1964","journal-title":"Proc. Natl. Acad. Sci. USA"},{"issue":"6","key":"10.1016\/j.apal.2022.103212_br0140","first-page":"1679","article-title":"From conventional to institution-independent logic programming","volume":"27","author":"\u0162utu","year":"2017","journal-title":"J. Log. Comput."},{"issue":"3\u20134","key":"10.1016\/j.apal.2022.103212_br0150","first-page":"321","article-title":"Institution-independent ultraproducts","volume":"55","author":"Diaconescu","year":"2003","journal-title":"Fundam. Inform."},{"issue":"3","key":"10.1016\/j.apal.2022.103212_br0160","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1093\/logcom\/exi082","article-title":"Proof systems for institutional logic","volume":"16","author":"Diaconescu","year":"2006","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.apal.2022.103212_br0170","series-title":"Institution-Independent Model Theory","author":"Diaconescu","year":"2008"},{"issue":"3","key":"10.1016\/j.apal.2022.103212_br0180","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1093\/logcom\/ext016","article-title":"Quasi-varieties and initial semantics for hybridized institutions","volume":"26","author":"Diaconescu","year":"2016","journal-title":"J. Log. Comput."},{"issue":"5","key":"10.1016\/j.apal.2022.103212_br0190","first-page":"1577","article-title":"Implicit Kripke semantics and ultraproducts in stratified institutions","volume":"27","author":"Diaconescu","year":"2017","journal-title":"J. Log. Comput."},{"issue":"5","key":"10.1016\/j.apal.2022.103212_br0200","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1017\/S0960129514000383","article-title":"Encoding hybridised institutions into first-order logic","volume":"26","author":"Diaconescu","year":"2016","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"10.1016\/j.apal.2022.103212_br0210","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","article-title":"Institutions: abstract model theory for specification and programming","volume":"39","author":"Goguen","year":"1992","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.apal.2022.103212_br0220","first-page":"163","article-title":"Definability of sets in models of axiomatic theories","volume":"9","author":"Grzegorczyk","year":"1961","journal-title":"Bull. Acad. Pol. Sci., S\u00e9r. Sci. Math. Astron. Phys."},{"key":"10.1016\/j.apal.2022.103212_br0230","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1016\/j.tcs.2012.12.002","article-title":"Interpolation in logics with constructors","volume":"474","author":"G\u0103in\u0103","year":"2013","journal-title":"Theor. Comput. Sci."},{"issue":"3\u20134","key":"10.1016\/j.apal.2022.103212_br0240","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s11787-013-0090-0","article-title":"Forcing, Downward L\u00f6wenheim-Skolem and omitting types theorems, institutionally","volume":"8","author":"G\u0103in\u0103","year":"2014","journal-title":"Log. Univers."},{"issue":"5","key":"10.1016\/j.apal.2022.103212_br0250","doi-asserted-by":"crossref","first-page":"805","DOI":"10.1007\/s00165-016-0414-y","article-title":"Birkhoff style calculi for hybrid logics","volume":"29","author":"G\u0103in\u0103","year":"2017","journal-title":"Form. Asp. Comput."},{"issue":"6","key":"10.1016\/j.apal.2022.103212_br0260","doi-asserted-by":"crossref","first-page":"1717","DOI":"10.1093\/logcom\/exv018","article-title":"Downward L\u00f6wenheim-Skolem Theorem and interpolation in logics with constructors","volume":"27","author":"G\u0103in\u0103","year":"2017","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.apal.2022.103212_br0270","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2017.04.009","article-title":"Foundations of logic programming in hybrid logics with user-defined sharing","volume":"686","author":"G\u0103in\u0103","year":"2017","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"10.1016\/j.apal.2022.103212_br0280","doi-asserted-by":"crossref","DOI":"10.1145\/3400294","article-title":"Forcing and calculi for hybrid logics","volume":"67","author":"G\u0103in\u0103","year":"2020","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.apal.2022.103212_br0290","series-title":"14th Conference on Advances in Modal Logic","first-page":"407","article-title":"Robinson consistency in many-sorted hybrid first-order logics","author":"G\u0103in\u0103","year":"2022"},{"key":"10.1016\/j.apal.2022.103212_br0300","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, Proceedings","first-page":"277","article-title":"Birkhoff completeness for hybrid-dynamic first-order logic","volume":"vol. 11714","author":"G\u0103in\u0103","year":"2019"},{"key":"10.1016\/j.apal.2022.103212_br0310","series-title":"25th Asia-Pacific Software Engineering Conference","first-page":"99","article-title":"Specification and verification of invariant properties of transition systems","author":"G\u0103in\u0103","year":"2018"},{"issue":"1","key":"10.1016\/j.apal.2022.103212_br0320","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1093\/logcom\/exs044","article-title":"Initial semantics in logics with constructors","volume":"25","author":"G\u0103in\u0103","year":"2015","journal-title":"J. Log. Comput."},{"issue":"16","key":"10.1016\/j.apal.2022.103212_br0330","first-page":"2204","article-title":"Constructor-based logics","volume":"18","author":"G\u0103in\u0103","year":"2012","journal-title":"J. Univers. Comput. Sci."},{"issue":"6","key":"10.1016\/j.apal.2022.103212_br0340","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1093\/logcom\/exq012","article-title":"Completeness by forcing","volume":"20","author":"G\u0103in\u0103","year":"2010","journal-title":"J. Log. Comput."},{"key":"10.1016\/j.apal.2022.103212_br0350","doi-asserted-by":"crossref","unstructured":"Daniel G\u0103in\u0103, Min Zhang, Yuki Chiba, Yasuhito Arimoto, Constructor-Based Inductive Theorem Prover, See [39] (2013) 328\u2013333.","DOI":"10.1007\/978-3-642-40206-7_26"},{"key":"10.1016\/j.apal.2022.103212_br0360","series-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag","year":"1993"},{"issue":"4","key":"10.1016\/j.apal.2022.103212_br0370","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1145\/115234.115351","article-title":"A propositional modal logic of time intervals","volume":"38","author":"Halpern","year":"1991","journal-title":"J. ACM"},{"issue":"1","key":"10.1016\/j.apal.2022.103212_br0380","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/568438.568456","article-title":"Dynamic logic","volume":"32","author":"Harel","year":"2001","journal-title":"SIGACT News"},{"key":"10.1016\/j.apal.2022.103212_br0390","series-title":"Algebra and Coalgebra in Computer Science - 5th International Conference, Proceedings","volume":"vol. 8089","year":"2013"},{"key":"10.1016\/j.apal.2022.103212_br0400","doi-asserted-by":"crossref","first-page":"183","DOI":"10.2307\/2268617","article-title":"A generalization of the concept of omega-consistency","volume":"19","author":"Henkin","year":"1954","journal-title":"J. Symb. Log."},{"key":"10.1016\/j.apal.2022.103212_br0410","doi-asserted-by":"crossref","first-page":"87","DOI":"10.4064\/fm170-1-5","article-title":"Categoricity without equality","volume":"170","author":"Keisler","year":"2001","journal-title":"Fundam. Math."},{"issue":"3","key":"10.1016\/j.apal.2022.103212_br0420","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1111\/j.1755-2567.1978.tb00174.x","article-title":"Omitting uncountable types and extensions of elementary logic","volume":"44","author":"Lindstr\u00f6m","year":"1978","journal-title":"Theoria"},{"key":"10.1016\/j.apal.2022.103212_br0430","series-title":"Algebra and Coalgebra in Computer Science - 4th International Conference, Proceedings","first-page":"283","article-title":"Hybridization of institutions","volume":"vol. 6859","author":"Martins","year":"2011"},{"key":"10.1016\/j.apal.2022.103212_br0440","doi-asserted-by":"crossref","unstructured":"Renato Neves, Alexandre Madeira, Manuel A. Martins, Lu\u00eds Soares Barbosa, Hybridisation at Work, See [39] (2013) 340\u2013345.","DOI":"10.1007\/978-3-642-40206-7_28"},{"key":"10.1016\/j.apal.2022.103212_br0450","doi-asserted-by":"crossref","first-page":"246","DOI":"10.2307\/2269096","article-title":"On \u03c9-consistency and related properties","volume":"21","author":"Orey","year":"1956","journal-title":"J. Symb. Log."},{"issue":"2","key":"10.1016\/j.apal.2022.103212_br0460","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0890-5401(91)90026-X","article-title":"An essay in combinatory dynamic logic","volume":"93","author":"Passay","year":"1991","journal-title":"Inf. Comput."},{"key":"10.1016\/j.apal.2022.103212_br0470","series-title":"Algebra and Coalgebra in Computer Science, Second International Conference, Proceedings","first-page":"409","article-title":"An institutional version of G\u00f6del's completeness theorem","volume":"vol. 4624","author":"Petria","year":"2007"},{"key":"10.1016\/j.apal.2022.103212_br0480","series-title":"Past, Present and Future","author":"Prior","year":"1967"},{"key":"10.1016\/j.apal.2022.103212_br0490","first-page":"69","article-title":"Forcing in model theory","volume":"5","author":"Robinson","year":"1971","journal-title":"Symp. Math."},{"key":"10.1016\/j.apal.2022.103212_br0500","series-title":"Handbook of Logic and Language","first-page":"475","article-title":"Chapter 8 - feature logics","author":"Rounds","year":"1997"},{"key":"10.1016\/j.apal.2022.103212_br0510","series-title":"Saturated Model Theory","author":"Sacks","year":"1972"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007222001270?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007222001270?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T10:12:58Z","timestamp":1759140778000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007222001270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3]]},"references-count":51,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["S0168007222001270"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2022.103212","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2023,3]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Omitting types theorem in hybrid dynamic first-order logic with rigid symbols","name":"articletitle","label":"Article Title"},{"value":"Annals of Pure and Applied Logic","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.apal.2022.103212","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2022 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"103212"}}