The Computational Complexity of Provability in Systems of Modal Propositional Logic
Richard E. Ladner · SIAM Journal on Computing · 1977
The computational complexity of the provability problem in systems of modal propositional logic is investigated. Every problem computable in polynomial space is $\log $ space reducible to the provability problem in any modal system between K and $S4$. In particular, the provability problem in K, T, and $S4$ are $\log $ space complete in polynomial space. The nonprovability problem in $S5$ is $\log $ space complete in nondeterministic polynomial time.