From: Gerwin Klein <kleing@unsw.edu.au>
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL
by Christoph Benzmüller and Sebastian Reiche
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.
https://www.isa-afp.org/entries/PAL.html
Enjoy!
Gerwin
Last updated: Jul 15 2022 at 23:21 UTC