Dynamic Logic of Common Knowledge in a Proof Assistant

Abstract : Common Knowledge Logic is meant to describe situations of the real world where a group of agents is involved. These agents share knowledge and make strong statements on the knowledge of the other agents (the so called common knowledge). But as we know, the real world changes and overall information on what is known about the world changes as well. The changes are described by dynamic logic. To describe knowledge changes, dynamic logic should be combined with logic of common knowledge. In this paper we describe experiments which we have made about the integration in a unique framework of common knowledge logic and dynamic logic in the proof assistant Coq. This results in a set of fully checked proofs for readable statements. We describe the framework and how a proof can be conducted
Type de document :
Pré-publication, Document de travail
LIP Research Report RR2007-50. 15 p. 2007
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00198782
Contributeur : Pierre Lescanne <>
Soumis le : mardi 18 décembre 2007 - 11:42:55
Dernière modification le : mardi 24 avril 2018 - 13:52:38
Document(s) archivé(s) le : lundi 12 avril 2010 - 08:14:55

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : ensl-00198782, version 1
  • ARXIV : 0712.3146

Collections

Citation

Pierre Lescanne, Jérôme Puisségur. Dynamic Logic of Common Knowledge in a Proof Assistant. LIP Research Report RR2007-50. 15 p. 2007. 〈ensl-00198782〉

Partager

Métriques

Consultations de la notice

314

Téléchargements de fichiers

101