---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Jakub
foaf_name: Michaliszyn, Jakub
foaf_surname: Michaliszyn
- foaf_Person:
foaf_givenName: Jan
foaf_name: Otop, Jan
foaf_surname: Otop
foaf_workInfoHomepage: http://www.librecat.org/personId=2FC5DA74-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Emanuel
foaf_name: Kieroňski, Emanuel
foaf_surname: Kieroňski
bibo_doi: 10.1145/2817825
bibo_issue: '1'
bibo_volume: 17
dct_date: 2015^xs_gYear
dct_language: eng
dct_publisher: ACM@
dct_title: On the decidability of elementary modal logics@
...