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.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|