We establish the complexity of decision problems associated with the nonmonotonic modal logic S4. We prove that the problem of existence of an S4-expansion for a given set A of premisses is ΣP2-complete. Similarly, we show that for a given formula Φ and a set A of premisses, it is ΣP2-complete to decide whether Φ belongs to at least one S4-expansion for A, and it is πP2-complete to decide whether Φ belongs to all S4-expansions for A. This refutes a conjecture of Gottlob that these problems are PSPACE-complete. An interesting aspect of these results is that reasoning (testing satisfiability and provability) in the monotonic modal logic S4 is PSPACE-complete. To the best of our knowledge, the nonmonotonic logic S4 is the first example of a nonmonotonic formalism which is computationally easier than the monotonic logic that underlies it (assuming PSPACE does not collapse to ΣP2).

Intuitively clear Kripke-style semantics for nonmonotonic modal logic are provided. Minimal model semantics is defined, and soundness and completeness of the semantics for nonmonotonic modal logics are proved. It is shown how the semantics looks for some most popular or most interesting modal logics. Applications to finding expansions and comparing nonmonotonic logics based on different monotonic modal logics are presented. A few examples of using the semantics for obtaining intuitively clear proofs of some results of nonmonotonic modal logics are given.>