Mechanizing epistemic logic with Coq

Pierre Lescanne (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

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-12

Mots clés: Epistemic Logic; Mechanizing Logic; Modal Logic

Mots clés: logique épistémique; mécanisation de la logique; logique modale

Domaines: Informatique [cs]

Pierre Lescanne. Mechanizing epistemic logic with Coq. [Research Report] LIP RR-2004-27, Laboratoire de l'informatique du parallélisme. 2004, 2+14p. ⟨hal-02102004⟩