Epistemic Logic in Higher Order Logic An experiment with COQ

(eng) We present an experiment on epistemic logic, also called knowledge logic, we have done using COQ. This work involves a formalization in COQ of the epistemic logic which has been checked for adequacy on two puzzles well known in the community. COQ is a proof assistant which implements a higher logic known as the calculus of inductive construction and which provides a convenient framework to embed logics like epistemic logic. We try to draw from this exercise lessons for future works. protocols