Common knowledge logic in a higher order proof assistant - ENS de Lyon - École normale supérieure de Lyon Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Common knowledge logic in a higher order proof assistant

Résumé

This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a certain proposition in a inductive way. This modality is specified by using a fixpoint approach. Furthermore, from these experiments, we discuss and compare the structure of theorems that can be proved in specific theories that use common knowledge logic. Those structures manifests the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.
Fichier principal
Vignette du fichier
common_know_logic.pdf (186.79 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

ensl-00199368 , version 1 (18-12-2007)
ensl-00199368 , version 2 (15-01-2008)
ensl-00199368 , version 3 (15-03-2019)

Identifiants

Citer

Pierre Lescanne. Common knowledge logic in a higher order proof assistant. Common knowledge logic in a higher order proof assistant, Max Planck Institute for Informatics, Jul 2013, Saarbrück, Germany. pp.271-284. ⟨ensl-00199368v2⟩

Collections

LIP_PLUME
135 Consultations
402 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More