### 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.

### License

BSD License

### Topics

- Logic/General logic/Logics of knowledge and belief

### Session PAL

- PAL

## Cite

×

PAL-AFP

    @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   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/PAL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Nov 14, 2021 : Isabelle2021