HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

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.
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

Contributor : Pierre Lescanne Connect in order to contact the contributor
Submitted on : Friday, March 15, 2019 - 11:40:57 AM
Last modification on : Saturday, September 11, 2021 - 3:19:12 AM


Files produced by the author(s)




Pierre Lescanne. Common knowledge logic in a higher order proof assistant. Andreï Voronkov & Christoph Weidenbach. Memory of Harald Ganzinger 2013, 7797, Springer, pp.271-284, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-40206-7_15⟩. ⟨ensl-00199368v3⟩



Record views


Files downloads