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 premises is Σ2 P-complete. Similarly, we show that for a given formula ϕ and a set A of premises, it is Σ2 P-complete to decide whether ϕ belongs to at least one S4-expansion for A, and it is Π2 P-complete to decide whether ϕ belongs to all S4-expansions for A. 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 nonmonotoific formalism which is computationally easier than the monotonic logic that underlies it (assuming PSPACE does not collapse to Σ2 P).
|Title of host publication||Computational Logic and Proof Theory - 3rd Kurt Godel Colloquium, KGC 1993, Proceedings|
|Editors||Georg Gottlob, Alexander Leitsch, Daniele Mundici|
|Number of pages||12|
|State||Published - 1993|
|Event||3rd Kurt Godel Colloquium on Computational Logic and Proof Theory, KGC 1993 - Brno, Czech Republic|
Duration: Aug 24 1993 → Aug 27 1993
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||3rd Kurt Godel Colloquium on Computational Logic and Proof Theory, KGC 1993|
|Period||8/24/93 → 8/27/93|
Bibliographical notePublisher Copyright:
© Springer-Verlag Berlin Heidelberg 1993.
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science (all)