Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

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.

Cite

Text

Halpern and Rêgo. "Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic." International Joint Conference on Artificial Intelligence, 2007. doi:10.1093/logcom/exm029

Markdown

[Halpern and Rêgo. "Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic." International Joint Conference on Artificial Intelligence, 2007.](https://mlanthology.org/ijcai/2007/halpern2007ijcai-characterizing-a/) doi:10.1093/logcom/exm029

BibTeX

@inproceedings{halpern2007ijcai-characterizing-a,
  title     = {{Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic}},
  author    = {Halpern, Joseph Y. and Rêgo, Leandro Chaves},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2007},
  pages     = {2306-2311},
  doi       = {10.1093/logcom/exm029},
  url       = {https://mlanthology.org/ijcai/2007/halpern2007ijcai-characterizing-a/}
}