Common knowledge logic in a higher order proof assistant

Abstract : 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.
Type de document :
Communication dans un congrès
Andreï Voronkov & Christoph Weidenbach. Common knowledge logic in a higher order proof assistant, Jul 2013, Saarbrück, Germany. Springer, 7797, pp.271-284, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00199368
Contributeur : Pierre Lescanne <>
Soumis le : mardi 15 janvier 2008 - 14:43:21
Dernière modification le : mardi 24 avril 2018 - 13:52:31
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:11:23

Fichiers

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

Identifiants

  • HAL Id : ensl-00199368, version 2
  • ARXIV : 0712.3147

Collections

Citation

Pierre Lescanne. Common knowledge logic in a higher order proof assistant. Andreï Voronkov & Christoph Weidenbach. Common knowledge logic in a higher order proof assistant, Jul 2013, Saarbrück, Germany. Springer, 7797, pp.271-284, 2013, Lecture Notes in Computer Science. 〈ensl-00199368v2〉

Partager

Métriques

Consultations de la notice

207

Téléchargements de fichiers

340