Nonmonotonic Reasoning is Sometimes Simpler

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 P 2 -complete. Similarly, we show that for a given formula ' and a set A of premises, it is P 2 complete to decide whether ' belongs to at least one S4-expansion for A, and it is P 2 -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 satis ability and provability) in the monotonic modal logic S4 is PSPACE-complete. To the best of our knowledge, the nonmonotonic logic S4 is the rst example of a nonmonotonic formalism which is computationally easier than the monotonic logic that underlies it (assuming PSPACE does not collapse to P 2 ).

• Type: Conference
• Year: 1993
• Where: KGC
• Authors: Grigori Schwarz, Miroslaw Truszczynski
• Keywords: Automated Reasoning, KGC 1993, Logic S4, Modal Logic S4, Nonmonotonic Modal Logic