  The formal system of intuitionistic epistemic logic IEL was proposed by S.
Artemov and T. Protopopescu. It provides the formal foundation for the study of
knowledge from an intuitionistic point of view based on
Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free
sequent calculus for IEL and establish that polynomial space is sufficient for
the proof search in it. So, we prove that IEL is PSPACE-complete.
