Mechanizing common knowledge logic using COQ

This paper proposes a formalization in COQ of common knowledge logic and checks its adequacy on case studies. This exercise allows 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. This work is experimental by nature as it tries to draw conclusions from experiments with a proof assistant.

• Type: Journal
• Year: 2006
• Where: AMAI
• Authors: Pierre Lescanne
• Keywords: AMAI 2006, Artificial Intelligence, Common Knowledge Logic, Order Common Knowledge, Proof Assistant