---
_id: '1680'
abstract:
- lang: eng
text: We consider the satisfiability problem for modal logic over first-order definable
classes of frames.We confirm the conjecture from Hemaspaandra and Schnoor [2008]
that modal logic is decidable over classes definable by universal Horn formulae.
We provide a full classification of Horn formulae with respect to the complexity
of the corresponding satisfiability problem. It turns out, that except for the
trivial case of inconsistent formulae, local satisfiability is eitherNP-complete
or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete,
or ExpTime-complete. We also show that the finite satisfiability problem for modal
logic over Horn definable classes of frames is decidable. On the negative side,
we show undecidability of two related problems. First, we exhibit a simple universal
three-variable formula defining the class of frames over which modal logic is
undecidable. Second, we consider the satisfiability problem of bimodal logic over
Horn definable classes of frames, and also present a formula leading to undecidability.
article_number: '2'
author:
- first_name: Jakub
full_name: Michaliszyn, Jakub
last_name: Michaliszyn
- first_name: Jan
full_name: Otop, Jan
id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
last_name: Otop
- first_name: Emanuel
full_name: Kieroňski, Emanuel
last_name: Kieroňski
citation:
ama: Michaliszyn J, Otop J, Kieroňski E. On the decidability of elementary modal
logics. ACM Transactions on Computational Logic. 2015;17(1). doi:10.1145/2817825
apa: Michaliszyn, J., Otop, J., & Kieroňski, E. (2015). On the decidability
of elementary modal logics. ACM Transactions on Computational Logic. ACM.
https://doi.org/10.1145/2817825
chicago: Michaliszyn, Jakub, Jan Otop, and Emanuel Kieroňski. “On the Decidability
of Elementary Modal Logics.” ACM Transactions on Computational Logic. ACM,
2015. https://doi.org/10.1145/2817825.
ieee: J. Michaliszyn, J. Otop, and E. Kieroňski, “On the decidability of elementary
modal logics,” ACM Transactions on Computational Logic, vol. 17, no. 1.
ACM, 2015.
ista: Michaliszyn J, Otop J, Kieroňski E. 2015. On the decidability of elementary
modal logics. ACM Transactions on Computational Logic. 17(1), 2.
mla: Michaliszyn, Jakub, et al. “On the Decidability of Elementary Modal Logics.”
ACM Transactions on Computational Logic, vol. 17, no. 1, 2, ACM, 2015,
doi:10.1145/2817825.
short: J. Michaliszyn, J. Otop, E. Kieroňski, ACM Transactions on Computational
Logic 17 (2015).
date_created: 2018-12-11T11:53:26Z
date_published: 2015-09-01T00:00:00Z
date_updated: 2021-01-12T06:52:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2817825
ec_funded: 1
intvolume: ' 17'
issue: '1'
language:
- iso: eng
month: '09'
oa_version: None
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication: ACM Transactions on Computational Logic
publication_status: published
publisher: ACM
publist_id: '5468'
quality_controlled: '1'
status: public
title: On the decidability of elementary modal logics
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 17
year: '2015'
...