Terminating Tableaux for Dynamic Epistemic Logics
(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:
https://lup.lub.lu.se/record/4017410
- author
- Hansen, Jens Ulrik LU
- publishing date
- 2010
- 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
- 2016-04-01 13:53:45
- date last changed
- 2022-01-27 21:43:43
@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}},
keywords = {{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}},
doi = {{10.1016/j.entcs.2010.04.011}},
volume = {{262}},
year = {{2010}},
}