Please use this identifier to cite or link to this item:
Title: A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
Authors: Frittella, S.
Greco, G.
Kurz, Alexander H.
Palmigiano, A.
Sikimić, V.
First Published: 3-Nov-2014
Publisher: Oxford University Press (OUP)
Citation: Journal of Logic and Computation, 2014, Special Issue on Substructural Logic and Information Dynamics
Abstract: 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.
DOI Link: 10.1093/logcom/exu063
ISSN: 0955-792X
eISSN: 1465-363X
Version: Post-print
Status: Peer-reviewed
Type: Other
Rights: Archived with reference to SHERPA/RoMEO and publisher website. © The Author, 2014. This is a pre-copyedited, author-produced PDF of an article accepted for publication in the Journal of Logic and Computation following peer review. The version of record J Logic Computation (2014) is available online at:
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
proof-theoretic-semantics-deak.pdfPost-review (final submitted)835.86 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.