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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00199368
Contributor : Pierre Lescanne <>
Submitted on : Tuesday, December 18, 2007 - 6:13:32 PM
Last modification on : Friday, April 20, 2018 - 3:44:24 PM
Long-term archiving on : Monday, April 12, 2010 - 8:24:42 AM

Files

common_know_logic.pdf
Files produced by the author(s)

Identifiers

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

Collections

Citation

Pierre Lescanne. Common knowledge logic in a higher order proof assistant?. 2007. ⟨ensl-00199368v1⟩

Share

Metrics

Record views

7

Files downloads

17