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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Alberucci, L., Jäger, G.: About cut elimination for logics of common knowledge. Ann. Pure Appl. Logic 133, 73–99 (2005)
Aumann, R.J.: Agreeing to disagree. Ann. Stat. 4(6), 1236–1239 (1976)
Aumann, R.J.: Backward induction and common knowledge of rationality. Games Econom. Behav. 8, 6–19 (1995)
Avron, A., Honsell, F., Mason, I.A.: An overview of the Edinburgh logical framework. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 323–340. Springer, Berlin Heidelberg New York (1989)
Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding modal logics in logical frameworks. Stud. Log. 60(1), 161–208 (1998)
Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.-C., Giménez, E., Herbelin, H., Huet, G., Laulhère, H., Muñoz, C., Murthy, C., Parent-Vigouroux, C., Loiseleur, P., Paulin-Mohring, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual. INRIA, version 6.3.11 edn (May 2000)
Basin, D.A., Matthews, S., Viganò, L.: Labelled propositional modal logics: theory and practic. J. Log. Comput. 7(6), 685–717 (1997)
Basin, D.A., Matthews, S., and Viganò, L.: Labelled modal logics: Quantifiers. J. Logic, Lang. Inf. 7(3), 237–263 (1998)
Ben-Ari, M., Halpern, J.Y., Pnueli, A.: Deterministic propositional dynamic logic: Finite models, complexity, and completeness. J. Comput. Syst. Sci. 25, 402–417 (1982)
van Benthem, J.: Games in dynamic epistemic logic. Bull. Econ. Res. 53(4), 219–248 (2001)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin Heidelberg New York (2004)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge, MA (1995)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194–211 (1979)
Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.): Epistemic and temporal logics, epistemic aspects of databases. In: Handbook of Logic in Artificial Intelligence and Logic Programming. Clarendon Press, Oxford, UK (1995)
Geanakoplos, J.: Common knowledge. In: Aumann, R., Hart, S. (eds.) Handbook of Game Theory, vol. 2, pp. 1437–1496. Elsevier, Amsterdam (1994)
Gordon, M.J.-C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge, UK (ISBN 0-521-44189-7) (1993)
Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. In: PODC ’84: Proceedings of the third annual ACM symposium on Principles of distributed computing, pp. 50–61, New York, NY. ACM, New York (1984)
Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell. 54(3), 319–379 (1992)
Halpern, J.Y., Reif, J.H.: The propositional dynamic logic of deterministic, well-structured programs. Theor. Comp. Sci. 27, 127–165 (1983)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge, MA (2000)
Howell, J., Kotz, D.: A formal semantics for SPKI. In: Proceedings of the Sixth European Symposium on Research in Computer Security (ESORICS 2000), pp. 140–158. Springer, Berlin Heidelberg New York (October 2000)
Kaneko, M.: Common knowledge logic and game logic. J. Symb. Log. 64(2), 685–700 (June 1999)
Lehmann, D.: Knowledge, common knowledge and related puzzles (extended summary). In: PODC ’84: Proceedings of the third annual ACM symposium on Principles of distributed computing, pp. 62–67, New York, NY. ACM, New York (1984)
Leibniz, G.W.: Discours de métaphysique. Published in [25], translated into English in [26] (1686)
Leibniz, G.W.: Discours de métaphysique. Collection historique des grands philosophes, vol. 1. In: Alcan, F. (ed.) Introduction et notes, par Henri Lestienne; préface de Auguste Penjon, Paris (1907) (available on http://gallica.bnf.fr/)
Leibniz, G.W.: Discourse on Metaphysics and the Monadology (trans. George R. Montgomery). Prometheus Books, Amherst, NY (1992) (first published by Open Court, 1908)
Lewis, D.: Convention: A Philosophical Study. Harvard University Press, Cambridge, MA (1969)
Liquori, L., Honsell, F., Lenisa, M.: A framework for defining logical frameworks. http://hal.inria.fr/inria-00088809 (August 2006)
Lismont, L.: Common knowledge: relating anti-founded situation semantics to modal logic neighbourhood semantics. J. Logic, Lang. Inf. 3, 285–302 (1995)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Constrcution and Analysis of Systems, TACA’96, volume 1055 of Lecture Notes in Computer Science, pp. 147–166 (1996)
Marrero, W., Clarke, E., Jha, S.: Model checking for security protocols. Technical Report CMU-CS-97-139, Carnegie Mellon University (1997)
McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 4, pp. 463–502. Edinburgh University Press (1969) http://www-formal.stanford.edu/jmc/mcchay69.pdf.
McCarthy, J., Sato, M., Hayashi, T., Igarashi, S. On the model theory of knowledge. Technical Report AIM-312, Stanford University (1977)
Meyer, J.-J.Ch., van der Hoek, W.: Epistemic logic for computer science and artificial intelligence. In: Cambridge Tracts in Theoretical Computer Science, vol. 41. Cambridge University Press, Cambridge, UK (1995)
Milgrom, P.: An axiomatic characterization of common knowledge. Econometrica 49(1), 219–222 (1981)
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P., (ed.) Logic in Computer Science. Academic, New York (1990)
Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Robust estimation. In: Numerical Recipes in FORTRAN: The Art of Scientific Computing, 2nd edn., pp. 694–700. Cambridge University Press, Cambridge, UK (1992)
Sato, M.: A study of Kripke-type models for some modal logics by Gentzen’s sequential method. Publ. Res. Inst. Math. Sci. 13(2), 381–468 (1977)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction, vol I. North Holland, Amsterdam, The Netherlands (1988)
Utas, G.: Robust Communications Software: Extreme Availability, Reliability and Scalability for Carrier-grade Systems. Wiley, New York (2005)
van Dalen, D.: Logic and Structure. Springer, Berlin Heidelberge New Yor (1994)
Vestergaard, R., Lescanne, P., Ono, H.: The inductive and modal proof theory of Aumann’s theorem on rationality. Technical Report IS-RR-2006-009, JAIST (2006) (available as http://www.jaist.ac.jp/~vester/Writings/vestergaard-IS-RR-2006-009.pdf)
de Wind, P.: Modal logic in COQ. Master’s thesis, Vrije Universiteit Amsterdam (2002) (available at http://www.cs.vu.nl/~pdwind/thesis/thesis.pdf)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Lescanne, P. Mechanizing common knowledge logic using COQ. Ann Math Artif Intell 48, 15–43 (2006). https://doi.org/10.1007/s10472-006-9042-1
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-006-9042-1