Colm Baston
The Coinductive Formulation of Common Knowledge
Baston, Colm; Capretta, Venanzio
Abstract
© 2018, Springer International Publishing AG, part of Springer Nature. 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.
Citation
Baston, C., & Capretta, V. (2018). The Coinductive Formulation of Common Knowledge. https://doi.org/10.1007/978-3-319-94821-8_8
Conference Name | ITP 2018 - Interactive Theorem Proving |
---|---|
Start Date | Oct 9, 2018 |
End Date | Jul 12, 2018 |
Acceptance Date | May 15, 2018 |
Online Publication Date | Jul 4, 2018 |
Publication Date | Jan 1, 2018 |
Deposit Date | Aug 6, 2018 |
Publicly Available Date | Mar 29, 2024 |
Publisher | Springer Verlag |
Volume | 10895 LNCS |
Pages | 126-141 |
Series Title | Lecture Notes in Computer Science |
Series Number | 10895 |
ISBN | 9783319948201 |
DOI | https://doi.org/10.1007/978-3-319-94821-8_8 |
Public URL | https://nottingham-repository.worktribe.com/output/953850 |
Publisher URL | https://link.springer.com/chapter/10.1007%2F978-3-319-94821-8_8 |
Additional Information | The final authenticated version is available online at https://doi.org/10.1007/978-3-319-94821-8_8. |
Files
Common Knowledge
(285 Kb)
PDF
You might also like
Game Forms for Coalition Effectivity Functions
(2019)
Conference Proceeding
A coalgebraic view of bar recursion and bar induction
(2016)
Journal Article
The continuity of monadic stream functions
(2017)
Conference Proceeding
Contractive Functions on Infinite Data Structures
(2016)
Conference Proceeding
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search