Every normal modal logic L gives rise to the consequence relation \phi |=L \psi which holds if, and only if, \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 \phi_1 and \phi_2, decide whether \phi_1\wedge \psi_2 is a conservative extension of \phi_1 in the sense that whenever \phi_1 \wedge \phi_2 |=L \psi and \psi does not contain propositional variables not occurring in \phi_1, then \phi_1 |=L \psi. We first prove that the conservativeness problem is coNExpTime-hard for all modal logics of unbounded width (which have rooted frames with more than N successors of the root, for any N < \omega). Then we show that this problem is (i) coNExpTime-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.
Conservative Extensions in Modal Logic / S. Ghilardi, C. Lutz, F. Wolter, M. Zakharyaschev - In: Advances in modal logic. Vol. 6 / edited by Guido Governatori, Ian Hodkinson and Yde Venema. / [a cura di] Guido Governatori, Ian Hodkinson, Yde Venema. - London : College Publications, 2006. - ISBN 1904987206. - pp. 187-207 (( convegno Advances in Modal Logic (AiML 06) tenutosi a Noosa - Queensland (Australia) nel 2006.
Conservative Extensions in Modal Logic
S. GhilardiPrimo
;
2006
Abstract
Every normal modal logic L gives rise to the consequence relation \phi |=L \psi which holds if, and only if, \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 \phi_1 and \phi_2, decide whether \phi_1\wedge \psi_2 is a conservative extension of \phi_1 in the sense that whenever \phi_1 \wedge \phi_2 |=L \psi and \psi does not contain propositional variables not occurring in \phi_1, then \phi_1 |=L \psi. We first prove that the conservativeness problem is coNExpTime-hard for all modal logics of unbounded width (which have rooted frames with more than N successors of the root, for any N < \omega). Then we show that this problem is (i) coNExpTime-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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.