University of Leicester
Browse

A proof-theoretic semantic analysis of dynamic epistemic logic

Download (835.86 kB)
journal contribution
posted on 2020-06-03, 14:00 authored by Frittella, Greco, AH Kurz, Palmigiano, Sikimic
The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem.

Funding

he research of the second and fourth author has been made possible by the NWO Vidi grant 016.138.314, by the NWO Aspasia grant 015.008.054, and by a Delft Technology Fellowship awarded in 2013 to the fourth author.

History

Citation

S. Frittella, G. Greco, A. Kurz, A. Palmigiano and V. Sikimić, "A proof-theoretic semantic analysis of dynamic epistemic logic," in Journal of Logic and Computation, vol. 26, no. 6, pp. 1961-2015, Dec. 2016, doi: 10.1093/logcom/exu063.

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • AM (Accepted Manuscript)

Published in

Journal of Logic and Computation

Volume

26

Issue

6

Pagination

1961-2015

Publisher

Oxford University Press (OUP)

eissn

1465-363X

Acceptance date

2014-11-03

Copyright date

2014

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC