Christian Hagemeier: Bachelor’s Thesis
Formalizing Intuitonistic Epistemic Logic in Coq
Advisors: Dominik Kirst and Holger Sturm
In this thesis, we formally verify selected results from formal epistemology in the proof assistant Coq.
In the first part, we will investigate intuitonistic epistemic logic (IEL) as introduced by Artemov.
IEL is an extension of intuitonistic propositional logic to accommodate reasoning about (single-agent) knowledge.
We verify soundness and completeness proofs and study connections to the Church-Fitch paradox.
Memos and milestones