Top

Published in:

2018 | OriginalPaper | Chapter

The Coinductive Formulation of Common Knowledge

Authors : Colm Baston, Venanzio Capretta

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We study the coinductive formulation of common knowledge in type theory. We formalise both the traditional relational semantics and an operator semantics, similar in form to the epistemic system S5, but at the level of events on possible worlds rather than as a logical derivation system. We have two major new results. Firstly, the operator semantics is equivalent to the relational semantics: we discovered that this requires a new hypothesis of semantic entailment on operators, not known in previous literature. Secondly, the coinductive version of common knowledge is equivalent to the traditional transitive closure on the relational interpretation. All results are formalised in the proof assistants Agda and Coq.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter A Coq Tactic for Equality Learning in Linear Arithmetic

next chapter Tactics and Certificates in Meta Dedukti

https://colmbaston.co.uk/files/Common-Knowledge.agda.

http://www.duplavis.com/venanzio/publications/common_knowledge.v.

Barwise, J.: Three views of common knowledge. In: Vardi, M.Y. (ed.) Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge, Pacific Grove, CA, March 1988, pp. 365–379. Morgan Kaufmann (1988)

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5CrossRefMATH

Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, New York (2001)CrossRef

Bucheli, S., Kuznets, R., Struder, T.: Two ways to common knowledge. Electron. Notes Theor. Comput. Sci. 262, 83–98 (2010)MathSciNetCrossRef

Capretta, V.: General recursion via coinductive types. Log. Methods Comput. Sci. 1(2), 1–18 (2005). https://doi.org/10.2168/LMCS-1(2:1)2005MathSciNetCrossRefMATH

Capretta, V.: Common knowledge as a coinductive modality. In: Barendsen, E., Geuvers, H., Capretta, V., Niqui, M. (eds.) Reflections on Type Theory, Lambda Calculus, and the Mind, pp. 51–61. ICIS, Faculty of Science, Radbout University Nijmegen (2007). Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday

Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58085-9_72CrossRef

Fagin, R., Halpern, J.Y., Vardi, M.Y., Moses, Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)MATH

Gamow, G., Stern, M.: Puzzle Math. Viking Press, New York (1958)MATH

10.

Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University (2016)

11.

Giménez, E.: Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60579-7_3CrossRef

12.

Hintikka, J.: Knowledge and Belief. Cornell University Press, Ithaca (1962)MATH

13.

Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_22CrossRef

14.

Kripke, S.A.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1–14 (1959)MathSciNetCrossRef

15.

Lescanne, P.: Common knowledge logic in a higher order proof assistant. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 271–284. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37651-1_11CrossRef

16.

Lewis, C.I., Langford, C.H.: Symbolic Logic. The Century Co., New York (1932)MATH

17.

Reynolds, J.C.: User-defined types and procedural data structures as complementary approaches to data abstraction. In: Gries, D. (ed.) Programming Methodology. MCS, pp. 309–317. Springer, New York (1978). https://doi.org/10.1007/978-1-4612-6315-9_22CrossRef

Title: The Coinductive Formulation of Common Knowledge
Authors: Colm Baston
Venanzio Capretta
Publisher: Springer International Publishing
Book: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_8

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner