(* File: Epistemic_Logic.thy Author: Asta Halkjær From 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). *) theory Epistemic_Logic imports Maximal_Consistent_Sets begin section ‹Syntax› type_synonym id = string