For nonlinear systems, the feedback design often provides only a locally asymptotically stable steady state. The domain of attraction of a steady state point is important for evaluating the control system. Lyapunov techniques are generally used to estimate domains of attraction, but their application is usually not straightforward. In certain cases, Lyapunov conditions can be solved using numerical approaches, e.g. with sum-of-squares methods (SoS), linear matrix inequalities (LMIs), or interval arithmetic. For polynomial systems, the inequalities resulting from the Lyapunov conditions can be solved formally using quantifier elimination. Quantifier elimination is a technique of simplifying a logical formula by removing quantifiers while producing an equivalent quantifier-free formula. Smooth nonlinearities can be enclosed by polynomial functions or embedded into higher dimensional polynomial systems. The calculation of bounds for domains of attraction is illustrated on various examples.