Conservative Extensions in Modal Logics

S. GhilardiS. Ghilardi, Carsten LutzCarsten Lutz, Frank WolterFrank Wolter, M. ZakharyaschevM. Zakharyaschev

Download

S. Ghilardi, Carsten Lutz, Frank Wolter, M. Zakharyaschev
Conservative Extensions in Modal Logics
In Guido Governatori and Ian Hodkinson and Yde Venema, eds., Advances in Modal Logics Volume 6, 187-207, 2006. College Publications

Details
Bibtex

KurzfassungAbstract
Every modal logic L gives rise to the consequence relation that relates formulas phi and psi iff psi is true in a world of an L-model whenever phi is true in that world. We consider the following algorithmic problem for L. Given two modal formulas phi1 and phi2, decide whether their conjunction is a conservative extension of phi1 in the sense that whenever psi is a consequence of the conjunction of phi1 and phi2 and psi does not contain propositional variables not occurring in phi1, then psi is already a consequence of phi1.. We first prove that the conservativeness problem is co-NExpTime-hard for all modal logics of unbounded width (which have rooted frames with more than N successors of the root, for any N smaller than omega. Then we show that this problem is (i) co-NExpTime-complete for S5 and K, (ii) in ExpSpace for S4 and (iii) ExpSpace-complete for GL.3 (the logic of finite strict linear orders). The proofs for S5 and K use the fact that these logics have uniform interpolants of exponential size.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ GhiLuWoZa-06,
  author = {S. {Ghilardi} and C. {Lutz} and F. {Wolter} and M. {Zakharyaschev}},
  booktitle = {Advances in Modal Logics Volume 6},
  editor = {Guido {Governatori} and Ian {Hodkinson} and Yde {Venema}},
  pages = {187--207},
  publisher = {College Publications},
  title = {Conservative Extensions in Modal Logics},
  year = {2006},
}