The complexity of some non-classical logics

Decision procedures for validity in intuitionistic propositional calculus and modal propositional calculus are given which require a running time proportional to a polynomial in the length of the formula on a nondeterministic Turing machine. Using a theorem of Cook´s and well-known transformations from intuitionistic to classical and modal to intuitionistic logics, the validity problem for intuitionistic and modal logics is shown to be polynomial equivalent to the validity problem for classical logic.