  It was proved by Sela and by the authors that every formula in the theory of
a free group $F$ is equivalent to a boolean combination of
$\exists\forall$-formulas. We also proved that the elementary theory of a free
group is decidable (there is an algorithm given a sentence to decide whether
this sentence belongs to $Th(F)$). In this paper we give an algorithm for
reduction of a first order formula over a free group to an equivalent boolean
combination of $\exists\forall$-formulas.
