Mechanizing epistemic logic with Coq

I present a mechanization of epistemic logic, also called knowledge logic, I have done using Coq. This work includes a formalization in Coq of epistemic logic and two case studies. This report is an updating of LIP report RR2001-12.Je présente une mécanisation de la logique épistémique, aussi appelée logique de la connaissance que j’ai réalisée en COQ. Ce travail inclue une formalisation en COQ et deux cas d’étude. Ce rapport est une mise à jour du rapport LIP RR2001-1