{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T06:37:04Z","timestamp":1773383824103,"version":"3.50.1"},"reference-count":38,"publisher":"Oxford University Press (OUP)","issue":"6","license":[{"start":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T00:00:00Z","timestamp":1651104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,8,24]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>A shallow semantical embedding for public announcement logic (PAL) with relativized common knowledge is presented. This embedding enables the first-time automation of this logic with off-the-shelf theorem provers for classical higher-order logic. It is demonstrated (i) how meta-theoretical studies can be automated this way and (ii) how non-trivial reasoning in the target logic (PAL), required for instance to obtain a convincing encoding and automation of the wise men puzzle, can be realized. Key to the presented semantical embedding is that evaluation domains are modelled explicitly and treated as an additional parameter in the encodings of the constituents of the embedded target logic; in previous related works, e.g. on the embedding of normal modal logics, evaluation domains were implicitly shared between meta-logic and target logic. The work presented in this article constitutes an important addition to the pluralist LogiKEy knowledge engineering methodology, which enables experimentation with logics and their combinations, with general and domain knowledge, and with concrete use cases\u2014all at the same time.<\/jats:p>","DOI":"10.1093\/logcom\/exac029","type":"journal-article","created":{"date-parts":[[2022,3,23]],"date-time":"2022-03-23T12:20:23Z","timestamp":1648038023000},"page":"1243-1269","source":"Crossref","is-referenced-by-count":4,"title":["Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy"],"prefix":"10.1093","volume":"33","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[{"name":"University of Bamberg , Faculty Information Systems and Applied Computer Science, An der Weberei 5, 96047 Bamberg, Germany, and FU Berlin, Department of Mathematics and Computer Science, Arnimalle 7, 14195 Berlin, Germany"}]},{"given":"Sebastian","family":"Reiche","sequence":"additional","affiliation":[{"name":"FU Berlin , Department of Mathematics and Computer Science, Arnimalle 7, 14195 Berlin, Germany"}]}],"member":"286","published-online":{"date-parts":[[2022,4,28]]},"reference":[{"key":"2023090708035145000_ref1","first-page":"43","article-title":"A tableau method for public announcement logics","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Balbiani"},{"key":"2023090708035145000_ref2","volume-title":"Normal Multimodal Logics: Automatic deduction and Logic Programming Extension","author":"Baldoni","year":"1998"},{"key":"2023090708035145000_ref3","article-title":"Dynamic epistemic logic","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Baltag","year":"2016"},{"key":"2023090708035145000_ref4","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1093\/logcom\/exx038","article-title":"Symbolic model checking for dynamic epistemic logic\u2014S5 and beyond","volume":"28","author":"van Benthem","year":"2018","journal-title":"Journal of Logic and Computation"},{"key":"2023090708035145000_ref5","doi-asserted-by":"crossref","first-page":"1620","DOI":"10.1016\/j.ic.2006.04.006","article-title":"Logics of communication and change","volume":"204","author":"van Benthem","year":"2006","journal-title":"Information and Computation"},{"key":"2023090708035145000_ref6","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","article-title":"Cut-elimination for quantified conditional logic","volume":"46","author":"Benzm\u00fcller","year":"2017","journal-title":"Journal of Philosophical Logic"},{"key":"2023090708035145000_ref7","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1016\/j.scico.2018.10.008","article-title":"Universal (meta-)logical reasoning: Recent successes","volume":"172","author":"Benzm\u00fcller","year":"2019","journal-title":"Science of Computer Programming"},{"key":"2023090708035145000_ref8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.dib.2019.103823","article-title":"Universal (meta-)logical reasoning: The wise men puzzle (Isabelle\/HOL dataset)","volume":"24","author":"Benzm\u00fcller","year":"2019","journal-title":"Data in Brief"},{"key":"2023090708035145000_ref9","article-title":"Church\u2019s type theory. Version: Summer 2019","author":"Benzm\u00fcller","year":"2019"},{"key":"2023090708035145000_ref10","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","article-title":"Higher-order semantics and extensionality","volume":"69","author":"Benzm\u00fcller","year":"2004","journal-title":"Journal of Symbolic Logic"},{"key":"2023090708035145000_ref11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.dib.2020.106409","article-title":"LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle\/HOL dataset)","volume":"33","author":"Benzm\u00fcller","year":"2020","journal-title":"Data in Brief"},{"key":"2023090708035145000_ref12","doi-asserted-by":"crossref","DOI":"10.1016\/B978-0-444-51624-4.50005-8","article-title":"Automation of higher-order logic","volume-title":"Handbook of the History of Logic, Volume 9\u2014Computational Logic","author":"Benzm\u00fcller","year":"2014"},{"key":"2023090708035145000_ref13","doi-asserted-by":"crossref","first-page":"103348","DOI":"10.1016\/j.artint.2020.103348","article-title":"Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support","volume":"287","author":"Benzm\u00fcller","year":"2020","journal-title":"Artificial Intelligence"},{"key":"2023090708035145000_ref14","doi-asserted-by":"crossref","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","article-title":"Multimodal and intuitionistic logics in simple type theory","volume":"18","author":"Benzm\u00fcller","year":"2010","journal-title":"The Logic Journal of the IGPL"},{"key":"2023090708035145000_ref15","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","article-title":"Quantified multimodal logics in simple type theory","volume":"7","author":"Benzm\u00fcller","year":"2013","journal-title":"Logica Universalis"},{"key":"2023090708035145000_ref16","first-page":"1","article-title":"Automating public announcement logic and the wise men puzzle in Isabelle\/HOL","author":"Benzm\u00fcller","year":"2021"},{"key":"2023090708035145000_ref17","first-page":"116","article-title":"Extending sledgehammer with SMT solvers","volume":"51","author":"Blanchette","year":"2011","journal-title":"Journal of Automated Reasoning"},{"key":"2023090708035145000_ref18","first-page":"131","article-title":"Nitpick: A counterexample generator for higher-order logic based on a relational model finder","volume-title":"Interactive Theorem Proving","author":"Blanchette"},{"key":"2023090708035145000_ref19","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"key":"2023090708035145000_ref20","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/j.entcs.2005.07.029","article-title":"Model checking Russian cards","volume":"149","author":"van Ditmarsch","year":"2006","journal-title":"Electronic Notes Theoretical Computer Science"},{"key":"2023090708035145000_ref21","first-page":"305","article-title":"DEMO\u2014A demo of epistemic modelling","volume-title":"Interactive Logic. Selected Papers from the 7th Augustus de Morgan Workshop","author":"van Eijck","year":"2007"},{"key":"2023090708035145000_ref22","article-title":"DEMO-S5","volume-title":"Technical Report","author":"van Eijck","year":"2014"},{"key":"2023090708035145000_ref23","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/S0168-0072(98)00033-5","article-title":"Common knowledge revisited","volume":"96","author":"Fagin","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"2023090708035145000_ref24","first-page":"479","article-title":"MCK: Model checking the logic of knowledge","volume-title":"Computer Aided Verification","author":"Gammie"},{"key":"2023090708035145000_ref25","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/2628136.2628138","article-title":"Folding domain-specific languages: Deep and shallow embeddings (functional pearl)","volume-title":"Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming","author":"Gibbons","year":"2014"},{"key":"2023090708035145000_ref26","first-page":"14","article-title":"Theorem provers for every normal modal logic","volume-title":"LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning","author":"Glei\u00dfner"},{"key":"2023090708035145000_ref27","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/BF01700692","article-title":"\u00dcber formal unentscheidbare S\u00e4tze der principia mathematica und verwandter systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"2023090708035145000_ref28","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"The Journal of Symbolic Logic"},{"key":"2023090708035145000_ref29","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s11229-013-0278-0","article-title":"Information dynamics and uniform substitution","volume":"190","author":"Holliday","year":"2013","journal-title":"Synthese"},{"key":"2023090708035145000_ref30","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1111\/phc3.12059","article-title":"Dynamic epistemic logic I: Modeling knowledge and belief","volume":"8","author":"Pacuit","year":"2013","journal-title":"Philosophy Compass"},{"key":"2023090708035145000_ref31","first-page":"199","article-title":"Higher-order abstract syntax","volume-title":"Proc. of the ACM SIGPLAN\u201988 Conference on Programming Language Design and Implementation (PLDI)","author":"Pfenning","year":"1988"},{"key":"2023090708035145000_ref32","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s11229-007-9168-7","article-title":"Logics of public communications","volume":"158","author":"Plaza","year":"2007","journal-title":"Synthese"},{"key":"2023090708035145000_ref33","first-page":"630","article-title":"Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation","volume-title":"Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2004","author":"Raimondi","year":"2004"},{"key":"2023090708035145000_ref34","first-page":"222","article-title":"Public announcement logic in HOL","volume-title":"Dynamic Logic. New Trends and Applications: Third International Workshop, DaL\u00ed 2020","author":"Reiche"},{"key":"2023090708035145000_ref35","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.cl.2015.07.003","article-title":"Combining deep and shallow embedding of domain-specific languages","volume":"44","author":"Svenningsson","year":"2015","journal-title":"Computer Languages, Systems and Structures"},{"key":"2023090708035145000_ref36","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Tobias"},{"key":"2023090708035145000_ref37","volume-title":"Dynamic Epistemic Logic","author":"Van Ditmarsch"},{"key":"2023090708035145000_ref38","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1111\/j.1755-2567.2011.01119.x","article-title":"Everything is knowable\u2014How to get to know whether a proposition is true","volume":"78","author":"Van Ditmarsch","year":"2012","journal-title":"Theoria"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/6\/1243\/51402383\/exac029.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/6\/1243\/51402383\/exac029.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T08:06:21Z","timestamp":1694073981000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/33\/6\/1243\/6575165"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,28]]},"references-count":38,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2022,4,28]]},"published-print":{"date-parts":[[2023,8,24]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exac029","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,9]]},"published":{"date-parts":[[2022,4,28]]}}}