%0 Journal Article %1 ladner:467 %A Ladner, Richard E. %D 1977 %I SIAM %J SIAM Journal on Computing %K complexity computational logic; modal %N 3 %P 467-480 %R 10.1137/0206033 %T The Computational Complexity of Provability in Systems of Modal Propositional Logic %U http://link.aip.org/link/?SMJ/6/467/1 %V 6 %X The computational complexity of the provability problem in systems of modal propositional logic is investigated. Every problem computable in polynomial space is $$ 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 $$ space complete in polynomial space. The nonprovability problem in $S5$ is $łog $ space complete in nondeterministic polynomial time.

@article{ladner:467, abstract = {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.}, added-at = {2007-11-23T14:13:20.000+0100}, author = {Ladner, Richard E.}, biburl = {https://www.bibsonomy.org/bibtex/2d09e045df5e654724aa4c8ea52e76751/ramaz}, doi = {10.1137/0206033}, interhash = {ddb24a2539ffd26019430e5c9c936a1f}, intrahash = {d09e045df5e654724aa4c8ea52e76751}, journal = {SIAM Journal on Computing}, keywords = {complexity computational logic; modal}, number = 3, pages = {467-480}, publisher = {SIAM}, timestamp = {2007-11-23T14:13:34.000+0100}, title = {The Computational Complexity of Provability in Systems of Modal Propositional Logic}, url = {http://link.aip.org/link/?SMJ/6/467/1}, volume = 6, year = 1977 }