We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q ⊆ P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas ζ(x) describing the isomorphism type of a local neighbourhood around its free variables x and statements of the form "the number of witnesses y of ψ(y) belongs to (Q+k)" where Q ∈ Q, k ∈ N, and ψ describes the isomorphism type of a local neighbourhood around its unique free variable y.

This paper's main result presents a 3-fold exponential algorithm that transforms a first-order formula φ together with a number d into a formula in Gaifman normal form that is equivalent to φ on the class of structures of degree at most d. For structures of polynomial growth, we even get a 2-fold exponential algorithm. These results are complemented by matching lower bounds: We show that for structures of degree 2, a 2-fold exponential blow-up in the size of formulas cannot be avoided. And for structures of degree 3, a 3-fold exponential blow-up is unavoidable. As a result of independent interest we obtain a 1-fold exponential algorithm which transforms a given first-order sentence φ of a very restricted shape into a sentence in Gaifman normal form that is equivalent to φ on all structures.