Mechanizing common knowledge logic using COQ |
| |
Authors: | Pierre Lescanne |
| |
Affiliation: | (1) Laboratoire de l’Informatique du Parallélisme, école Normale Supérieure de Lyon 46, Allée d’Italie, 69364 Lyon 07, France |
| |
Abstract: | 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.
|
| |
Keywords: | Common knowledge logic COQ Epistemic logic Higher order common knowledge logic Modalities |
本文献已被 SpringerLink 等数据库收录! |