Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy

A 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.