Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Automating Public Announcement ...

Email Gateway (Nov 14 2021 at 03:49):

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: Jan 04 2025 at 20:18 UTC