Epistemic Logic in Higher Order Logic An experiment with COQ - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2001

Epistemic Logic in Higher Order Logic An experiment with COQ

Résumé

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.
Nous rendons compte d'une expérimentation sur la logique épistémique, appelée aussi logique de la connaissances, que nous avons menée COQ. Ce travail implique la formalisation en COQ de la logique épistémique dont nous avons testé la pertinence sur deux vignettes bien connues dans la communauté. COQ est un assistant de preuve qui implant une logique d'ordre supérieur connue sous le nom de calcul des constructions inductif et sui offre un cadre commode pour y plonger la logique épistémique. Nous tentons de tirer de cet exercice des leçons pour des expérimentations ultérieures.
Fichier principal
Vignette du fichier
RR2001-12.pdf (203.15 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02101795 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101795 , version 1

Citer

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⟩
16 Consultations
114 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More