Many problems arising in real geometry can be formulated as first-order formulas. Thus quantifier elimination can be used to solve these problems. In this note, we discuss the applicability of implemented quantifier elimination algorithms for solving geometrical problems. In particular, we demonstrate how the tools of REDLOG can be applied to solve a real implicitization problem, namely the Enneper surface.
Erika Cetindag, Martin Griebl