Multi-type display calculus for dynamic epistemic logic

Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić

Research output: Contribution to JournalArticleAcademicpeer-review


In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.

Original languageEnglish
Pages (from-to)2017-2065
Number of pages49
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - 1 Jan 2016
Externally publishedYes


  • Display calculus
  • Dynamic epistemic logic
  • Modularity
  • Multi-type system


Dive into the research topics of 'Multi-type display calculus for dynamic epistemic logic'. Together they form a unique fingerprint.

Cite this