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
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02101795
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:06:31 AM
Last modification on : Wednesday, May 22, 2019 - 1:32:16 AM

File

RR2001-12.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101795, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

7

Files downloads

8