Mechanizing common knowledge logic using COQ
This paper presents a formalization in COQ of Common Knowledge Logic and checks its adequacy on case studies. Those studies allow exploring experimentally the proof-theoretic side of Common Knowledge Logic. This work is original in that nobody has considered Higher Order Common Knowledge Logic from the point of view of proofs performed on a proof assistant. As a matter of facts, it is experimental by nature as it tries to draw conclusions from experiments.
common knowledge logic coq higher order common knowledge logic epistemic logic modalities