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

 

Title: Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL
Authors: Christoph Benzm├╝ller and Sebastian Reiche
Submission date: 2021-11-08
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.
BibTeX:
@article{PAL-AFP,
  author  = {Christoph Benzm├╝ller and Sebastian Reiche},
  title   = {Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/PAL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.