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

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 consistency (i.e., nonprovability) 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

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: Joseph Y. Halpern, Leandro Chaves Rêgo
• Keywords: CORR 2006, Education, Great Deal, Modal Logic, Negative Introspection