Skip to Main content Skip to Navigation
Book sections

Common Knowledge Logic in a Higher Order Proof Assistant

Pierre Lescanne 1
1 LIP - Laboratoire de l'Informatique du Parallélisme
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 manifest the interplay between the theory (as implemented in the proof assistant Coq) and the metatheory.
Keywords : common knowledge logic higher order proof assistant COQ epistemic logic
Document type :
Book sections
Complete list of metadata
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00869081
Contributor : Pierre Lescanne <>
Submitted on : Wednesday, October 2, 2013 - 2:28:11 PM
Last modification on : Friday, June 25, 2021 - 3:40:04 PM

Identifiers

  • HAL Id : ensl-00869081, version 1

Collections

ENS-LYON | CNRS | INRIA | LIP | UNIV-LYON1 | UDL

Citation

Pierre Lescanne. Common Knowledge Logic in a Higher Order Proof Assistant. Andrei Voronkov, Christoph Weidenbach. Programming Logics - Essays in Memory of Harald Ganzinger., Springer, pp.271-284, 2013, Lecture Notes in Computer Science. ⟨ensl-00869081⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

162