  We stratify intuitionistic first-order logic over $(\forall,\to)$ into
fragments determined by the alternation of positive and negative occurrences of
quantifiers (Mints hierarchy).
  We study the decidability and complexity of these fragments. We prove that
even the $\Delta_2$ level is undecidable and that $\Sigma_1$ is
Expspace-complete. We also prove that the arity-bounded fragment of $\Sigma_1$
is complete for co-Nexptime.
