A. Avron, F. Honsell, M. Miculan, and C. Paravano, Encoding Modal Logics in Logical Frameworks, Studia Logica, vol.60, issue.1, pp.161-208, 1998.
DOI : 10.1023/A:1005060022386

A. Baltag, A logic of epistemic actions, Proceedings of the ESSLLI 1999 workshop on Foundations and Applications of Collective Agent-Based Systems (W. van der Hoek, 1999.

A. Baltag, L. Moss, and S. Solecki, The Logic of Public Announcements, Common Knowledge, and Private Suspicions, Proc. of TARK, 1998.
DOI : 10.1007/978-3-319-20451-2_38

J. Van-benthem, Exploring Logical Dynamics, 1996.

J. Van-benthem, Games in Dynamic-Epistemic Logic, Bulletin of Economic Research, vol.53, issue.4, pp.219-248, 2001.
DOI : 10.1111/1467-8586.00133

S. Coupet-grimal, An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions, Journal of Logic and Computation, vol.13, issue.6, pp.801-813, 2003.
DOI : 10.1093/logcom/13.6.801

J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, A Tutorial Introduction to PVS, 1995.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Y. Halpern and Y. Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, 1984.

D. Harel, First-Order Dynamic Logic, Lecture Notes in Computer Science, vol.68, 1979.
DOI : 10.1007/3-540-09237-4

D. Harel, J. Tiuryn, and D. Kozen, Dynamic Logic, 2000.

M. Kaufmann, J. S. Moore, and P. Manolios, Computer-Aided Reasoning: An Approach, 2000.

Y. Lafont, From proof nets to interaction nets Advances in Linear Logic, 1995.

D. Lehmann, Knowledge, common knowledge and related puzzles (Extended Summary), Proceedings of the third annual ACM symposium on Principles of distributed computing , PODC '84, 1984.
DOI : 10.1145/800222.806736

P. Lescanne, Mechanizing common knowledge logic using COQ, Annals of Mathematics and Artificial Intelligence, vol.13, issue.2, pp.15-43, 2006.
DOI : 10.1007/s10472-006-9042-1

H. J. Levesque and G. Lakemeyer, The Logic of Knowledge Bases, 2001.

J. Mccarthy, M. Sato, T. Hayashi, and S. Igarashi, On the Model Theory of Knowledge, 1977.

C. Raffalli, The PhoX Proof Assistant, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00396888

H. Team, The HOL System DESCRIPTION, 2005.

E. W. Weisstein, Kepler Conjecture, From MathWorld?A Wolfram Web Re- source