Name
Abstract | ||
|---|---|---|
Common knowledge logic is meant to describe situations of the real world where a group of agents is involved. These agents share knowledge and make strong hypotheses on the knowledge of the other agents (the so called common knowledge). But as we know, the real world changes and mostly information on what is known about the world changes as well. The changes are described by dynamic logic. To describe knowledge changes, dynamic logic should be combined with logic of common knowledge. In this paper we describe experiments which we have made about the integration in a unique framework of common knowledge logic and dynamic logic in the proof assistant COQ. This results in a set of fully checked proofs for readable statements. We describe the framework and how a proof can be conducted. |
Year | Venue | Keywords |
|---|---|---|
2007 | Clinical Orthopaedics and Related Research | dynamic logic,common knowledge,proof assistant.,proof assistant |
Field | DocType | Volume |
Computational logic,Mathematical economics,Autoepistemic logic,Programming language,Common knowledge (logic),Computer science,Description logic,Multimodal logic,Common knowledge,Bunched logic,Artificial intelligence,Dynamic logic (digital electronics) | Journal | abs/0712.3 |
Citations | PageRank | References |
3 | 0.47 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pierre Lescanne | 1 | 925 | 123.70 |
| Jérôme Puisségur | 2 | 3 | 0.47 |