[isabelle] new AFP entry: Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.