### Abstract

This work is a formalization of epistemic logic. It includes proofs of soundness and completeness for the axiom system K. The completeness proof is based on the textbook "Reasoning About Knowledge" by Fagin, Halpern, Moses and Vardi (MIT Press 1995). The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema (Cambridge University Press 2001). Papers: doi.org/10.1007/978-3-030-88853-4_1, doi.org/10.1007/978-3-030-90138-7_2.

### License

BSD License

### History

April 15, 2021
  Added completeness of modal logics T, KB, K4, S4 and S5.

### Topics

- Logic/General logic/Logics of knowledge and belief

### Session Epistemic_Logic

- Maximal_Consistent_Sets
- Epistemic_Logic

### Used by

- Stalnaker’s Epistemic Logic
- Public Announcement Logic

## Cite

×

Epistemic_Logic-AFP

    @article{Epistemic_Logic-AFP,
      author  = {Asta Halkjær From},
      title   = {Epistemic Logic: Completeness of Modal Logics},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Epistemic_Logic.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
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Oct 29, 2018 : Isabelle2018