Common knowledge logic in a higher order proof assistant
In: Memory of Harald Ganzinger 2013 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⟩ Programming Logics-Essays in Memory of Harald Ganzinger. Andrei Voronkov, Christoph Weidenbach. Programming Logics-Essays in Memory of Harald Ganzinger., Springer, pp.271-284, 2013, Lecture Notes in Computer Science Programming Logics ISBN: 9783642376504 Programming Logics; (2013-07-03)
Online
unknown
Zugriff:
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.
11 p
| Titel: |
Common knowledge logic in a higher order proof assistant
|
|---|---|
| Autor/in / Beteiligte Person: | Lescanne, Pierre ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; Andreï Voronkov & Christoph Weidenbach ; Andrei Voronkov, Christoph Weidenbach ; École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-École normale supérieure - Lyon (ENS Lyon) |
| Link: | |
| Quelle: | Memory of Harald Ganzinger 2013 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⟩ Programming Logics-Essays in Memory of Harald Ganzinger. Andrei Voronkov, Christoph Weidenbach. Programming Logics-Essays in Memory of Harald Ganzinger., Springer, pp.271-284, 2013, Lecture Notes in Computer Science Programming Logics ISBN: 9783642376504 Programming Logics; (2013-07-03) |
| Veröffentlichung: | HAL CCSD, 2013 |
| Medientyp: | unknown |
| ISBN: | 978-3-642-37650-4 (print) |
| Schlagwort: |
|
| Sonstiges: |
|