Public Announcement Logic in HOL

TL;DR

This paper introduces a novel shallow semantical embedding for public announcement logic with relativized common knowledge, enabling automation with existing theorem provers and facilitating complex reasoning tasks like the wise men puzzle.

Contribution

It presents the first automation of public announcement logic with relativized common knowledge using higher-order logic theorem provers, with explicit evaluation domains as a key innovation.

Findings

Automated meta-theoretical studies are possible with the embedding.

Complex reasoning tasks like the wise men puzzle can be encoded and automated.

Explicit modeling of evaluation domains improves the embedding's effectiveness.

Abstract

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 -- in contrast, e.g., to related work on the semantical embedding of normal modal logics -- is that evaluation domains are modeled explicitly and treated as additional parameter in the encodings of the constituents of the embedded target logic, while they were previously implicitly shared between meta logic and target logic.