Benzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Reiche, SebastianSebastianReiche2022-07-082022-07-0820231465-363X0955-792Xhttps://fis.uni-bamberg.de/handle/uniba/54497A shallow semantical embedding for public announcement logic 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 (public announcement logic), required e.g. 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 mod- eled explicitly and treated as an additional parameter in the encodings of the con- stituents of the embedded target logic; in previous related works, e.g. on the em- bedding 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 experimen- tation with logics and their combinations, with general and domain knowledge, and with concrete use cases — all at the same time.engPublic announcement logic; Relativized common knowledge; Semantical embedding; Higher-order logic; Proof automation004510article10.1093/logcom/exac029