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.
Christoph Benzmüller 🌐 and Sebastian Reiche 🌐
November 8, 2021