  In their seminal paper Artemov and Protopopescu provide Hilbert formal
systems, Brower-Heyting-Kolmogorov and Kripke semantics for the logics of
intuitionistic belief and knowledge. Subsequently Krupski has proved that the
logic of intuitionistic knowledge is PSPACE-complete and Su and Sano have
provided calculi enjoying the subformula property. This paper continues the
investigations around to sequent calculi for Intuitionistic Epistemic Logics by
providing sequent calculi that have the subformula property and that are
terminating in linear depth. Our calculi allow us to design a procedure that
for invalid formulas returns a Kripke model of minimal depth. Finally we also
discuss refutational sequent calculi, that is sequent calculi to prove the
invalidity.
