Original Articles |
Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic
Computer Science Department, Cornell University, USA. E-mail: halpern{at}cs.cornell.edu
Statistics Department, Federal University of Pernambuco, Brazil. E-mail: leandro{at}de.ufpe.br
Received 23 February 2007.
| Abstract |
|---|
There has been a great deal of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the satisfiability problem for all logics between K and S4 is PSPACE-hard, while for S5 it is NP-complete. We show that it is negative introspection, the axiom ¬Kp
K¬Kp, that causes the gap: if we add this axiom to any modal logic between K and S4, then the satisfiability problem becomes NP-complete. Indeed, the satisfiability problem is NP-complete for any modal logic that includes the negative introspection axiom.
Keywords: Euclidean Property; Negative Introspection; K5; S5; PSPACE; NP; Knowledge Representation