Multi-type display calculus for dynamic epistemic logic

Frittella, Sabine; Greco, G.; Kurz, Alexander; Palmigiano, A.; Sikimić, Vlasta

Multi-type display calculus for dynamic epistemic logic

Journal article (2016)

Authors

Sabine Frittella Aix Marseille Université

G. Greco

Alexander Kurz University of Leicester

A. Palmigiano

Vlasta Sikimić University of Belgrade

Modularity Display calculus Dynamic epistemic logic Multi-type system

To reference this document use:

http://resolver.tudelft.nl/uuid:9c5fb15d-9830-45aa-a674-a6b9ea5b2b2a

More Info

expand_more

Published Date

2016

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

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.