Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Epistemic Logic in Higher Order Logic An experiment with COQ

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:06:31 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:38 AM


Files produced by the author(s)


  • HAL Id : hal-02101795, version 1



Pierre Lescanne. Epistemic Logic in Higher Order Logic An experiment with COQ. [Research Report] LIP RR-2001-12, Laboratoire de l'informatique du parallélisme. 2001, 2+9p. ⟨hal-02101795⟩



Record views


Files downloads