Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL

Christoph Benzm├╝ller and Sebastian Reiche

8 November 2021

Abstract

We present a shallow embedding of public announcement logic (PAL) with relativized general knowledge in HOL. We then use PAL to obtain an elegant encoding of the wise men puzzle, which we solve automatically using sledgehammer.
BSD License

Topics

Theories