  We consider well-known provability logic GLP. We prove that the
GLP-provability problem for variable-free polymodal formulas is
PSPACE-complete. For a number n, let L^n_0 denote the class of all polymodal
variable-free formulas without modalities <n>, <n+1>,... . We show that, for
every number n, the GLP-provability problem for formulas from L^n_0 is in
PTIME.
