Abstract
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).
Original language | English |
---|---|
Title of host publication | Computational Logic and Proof Theory - 3rd Kurt Godel Colloquium, KGC 1993, Proceedings |
Editors | Georg Gottlob, Alexander Leitsch, Daniele Mundici |
Pages | 313-324 |
Number of pages | 12 |
DOIs | |
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 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 713 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 3rd Kurt Godel Colloquium on Computational Logic and Proof Theory, KGC 1993 |
---|---|
Country/Territory | Czech Republic |
City | Brno |
Period | 8/24/93 → 8/27/93 |
Bibliographical note
Publisher Copyright:© Springer-Verlag Berlin Heidelberg 1993.
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science