2006/03/05 by Joseph Y. Halpern, Leandro Chaves Rêgo, Halpern, Joseph Y. +1
Computer Science · #Advanced Algebra and Logic #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation
paper · pdf · doi:10.48550/arxiv.cs/0603019
openalex publication_date 2006/03/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
There has been a great of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the validity problem for all logics between K, T, and S4 is \sl PSPACE-complete, while for S5 it is \sl NP-complete. We show that, in a precise sense, it is negative introspection, the axiom ¬ K p \rimp K ¬ K p, that causes the gap. In a precise sense, if we require this axiom, then the satisfiability problem is \sl NP-complete; without it, it is \sl PSPACE-complete.