Christian Hagemeier: Bachelor’s Thesis

Saarland University Computer Science

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

Legal notice, Privacy policy