What is the computational complexity of intuitionistic propositional logic? Consider the decision problem: given formulas of propositional logic $\phi_1, \ldots, \phi_n, \psi$, determine whether $\phi_1, \ldots, \phi_n \vdash \psi$ intuitionistically.  This problem is well-known to be decidable, for example using an algorithm derived from the LJT* sequent calculus.  I was wondering if the computational complexity of this problem is known.

Trivially, the complexity is polynomial-equivalent to the complexity of the intuitionistic tautology problem: $\phi_1, \ldots, \phi_n \vdash \psi$ if and only if $\phi_1 \wedge \ldots \wedge \phi_n \rightarrow \psi$ is a tautology; and conversely, $\phi$ is a tautology if and only if $\vdash \phi$.
Certainly, the problem is co-NP-hard: as a corollary of the double-negation embedding, a formula $\phi$ is classically satisfiable if and only if $\lnot \phi$ is not a tautology of intuitionistic logic.

On the other hand, if I'm not mistaken, the problem is in PSPACE: the only rule of LJT* which could possibly increase the total length of a proof context is in the first subgoal of $(\alpha, \beta \rightarrow \gamma, \Gamma \vdash \beta) \wedge (\gamma, \Gamma \vdash \delta) \implies (\alpha \rightarrow \beta) \rightarrow \gamma, \Gamma \vdash \delta$.  But in that case, the second copy of $\beta$ should still be at most equal to the length of a formula in the original context.

(Also, since the Rieger-Nishimura lattice, the free Heyting algebra on one generator, has a simple computable description, the special case of this problem restricted to problems with a single atom would be in P.  That would be a severe restriction, though.)

Beyond that, in a quick Google search, I didn't find any results directly on this problem, just a few papers where the abstracts seemed to indicate they were considering fragments of propositional logic.  I also can't find any proof on my own which would refine the status.  (For example, for all I know, it might be possible that whenever the sequent is not intuitionistically valid, there exists a Kripke model of polynomial size which demonstrates this - in which case the problem would be co-NP-complete.  Or more generally, a Heyting algebra with a polynomial-size "description" would suffice.  It's harder for me to imagine some way to reduce a problem such as QBF to an instance of this problem to prove it's PSPACE-complete, though I also can't entirely rule out the possibility.)
A quick google search shows that the problem is PSPACE complete, a result apparently first proven by R. Statman.