# Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy

arXiv: https://arxiv.org/abs/2111.01654 · HTML: https://mlsanity.com/paper/2111.01654/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 38 references that are in the map.
- First posted on arXiv 2 Nov 2021.

## Builds on (most cited first, 1 of 1)

- [Public Announcement Logic in HOL](https://mlsanity.com/paper/2010.00810/) (2020)

## Built on by (most cited first, 3 of 3)

- [Automated Reasoning in Non-classical Logics in the TPTP World](https://mlsanity.com/paper/2202.09836/) (2022)
- [Faithful Logic Embeddings in HOL -- Deep and Shallow](https://mlsanity.com/paper/2502.19311/) (2025)
- [Normative Conditional Reasoning as a Fragment of HOL](https://mlsanity.com/paper/2308.10686/) (2023)

## Abstract (arXiv)

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 modeled 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 -- all at the same time.