What can one learn from implementing common knowledge logic in a higher order proof assistant
Pierre Lescanne · 2005
This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant C OQ. 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 inter- play between the theory (as implemented in the proof assistant C OQ) and the metatheory.