Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
Christoph Benzm\"uller, Sebastian Reiche

TL;DR
This paper introduces a semantical embedding approach for public announcement logic with relativized common knowledge, enabling automation with higher-order theorem provers and facilitating complex reasoning tasks like the wise men puzzle.
Contribution
It presents the first automation of this logic via off-the-shelf theorem provers and models evaluation domains explicitly, advancing the LogiKEy methodology.
Findings
Automated meta-theoretical reasoning in public announcement logic.
Successful encoding and automation of the wise men puzzle.
Explicit modeling of evaluation domains improves embedding accuracy.
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 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies · Logic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation
