The computational complexity of provability in systems of modal propositional logic

Abstract. The computational complexity of the provability problem in systems of modal proposi-tional logic is investigated. Every problem computable in polynomial space is log space reducible to the provability problem in any modal system between K and $4. In particular, the provability problem in K, T, and $4 are log space complete in polynomial space. The nonprovability problem in $5 is log space complete in nondeterministic polynomial time. Key words, modal logic, computational complexity Introduction. We investigate the computational complexity of deciding whether or not a modal propositional formula is provable in certain systems of modal propositional logic, including K, T, $4, and $5. In terms to be defined later we show (using a suggestion of S. K. Thomason) that if S is a modal system between K and $4, then every problem computable in polynomial space is lo