Skip to main content

Research Repository

Advanced Search

The Coinductive Formulation of Common Knowledge

Baston, Colm; Capretta, Venanzio

Authors

Colm Baston



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




You might also like



Downloadable Citations