Advanced

Terminating Tableaux for Dynamic Epistemic Logics

Hansen, Jens Ulrik LU (2010) In Electronical Notes in Theoretical Computer Science 262. p.141-156
Abstract
Throughout the last decade, there has been an increased interest in various forms of dynamic epistemic logics to model the flow of information and the effect this flow has on knowledge in multi-agent systems. This enterprise, however, has mostly been applicationally and semantically driven. This results in a limited amount of proof theory for dynamic epistemic logics.



In this paper, we try to compensate for a part of this by presenting terminating tableau systems for full dynamic epistemic logic with action models and for a hybrid public announcement logic (both without common knowledge). The tableau systems are extensions of already existing tableau systems, in addition to which we have used the reduction axioms of... (More)
Throughout the last decade, there has been an increased interest in various forms of dynamic epistemic logics to model the flow of information and the effect this flow has on knowledge in multi-agent systems. This enterprise, however, has mostly been applicationally and semantically driven. This results in a limited amount of proof theory for dynamic epistemic logics.



In this paper, we try to compensate for a part of this by presenting terminating tableau systems for full dynamic epistemic logic with action models and for a hybrid public announcement logic (both without common knowledge). The tableau systems are extensions of already existing tableau systems, in addition to which we have used the reduction axioms of dynamic epistemic logic to define rules for the dynamic part of the logics. Termination is shown using methods introduced by Braüner, Bolander, and Blackburn. (Less)
Please use this url to cite or link to this publication:
author
publishing date
type
Contribution to journal
publication status
published
subject
keywords
dynamic epistemic logic public announcement logic terminating tableau systems decision procedures hybrid logic reduction axioms
in
Electronical Notes in Theoretical Computer Science
volume
262
pages
141 - 156
publisher
Elsevier
external identifiers
  • scopus:79960140339
ISSN
1571-0661
DOI
10.1016/j.entcs.2010.04.011
language
English
LU publication?
no
id
e360d88e-eb11-4bef-babb-b5dec7a6371a (old id 4017410)
date added to LUP
2013-09-05 16:24:27
date last changed
2018-05-29 11:25:40
@article{e360d88e-eb11-4bef-babb-b5dec7a6371a,
  abstract     = {Throughout the last decade, there has been an increased interest in various forms of dynamic epistemic logics to model the flow of information and the effect this flow has on knowledge in multi-agent systems. This enterprise, however, has mostly been applicationally and semantically driven. This results in a limited amount of proof theory for dynamic epistemic logics.<br/><br>
<br/><br>
In this paper, we try to compensate for a part of this by presenting terminating tableau systems for full dynamic epistemic logic with action models and for a hybrid public announcement logic (both without common knowledge). The tableau systems are extensions of already existing tableau systems, in addition to which we have used the reduction axioms of dynamic epistemic logic to define rules for the dynamic part of the logics. Termination is shown using methods introduced by Braüner, Bolander, and Blackburn.},
  author       = {Hansen, Jens Ulrik},
  issn         = {1571-0661},
  keyword      = {dynamic epistemic logic public announcement logic terminating tableau systems decision procedures hybrid logic reduction axioms},
  language     = {eng},
  pages        = {141--156},
  publisher    = {Elsevier},
  series       = {Electronical Notes in Theoretical Computer Science},
  title        = {Terminating Tableaux for Dynamic Epistemic Logics},
  url          = {http://dx.doi.org/10.1016/j.entcs.2010.04.011},
  volume       = {262},
  year         = {2010},
}