Existential theory of the reals

In mathematical logic, computational complexity theory, and computer science, the existential theory of the reals is the set of all true sentences of the form

where ${\displaystyle F(X_{1},\dots X_{n})}$ is a quantifier-free formula involving equalities and inequalities of real polynomials.

The decision problem for the existential theory of the reals is the problem of finding an algorithm that decides, for each such formula, whether it is true or false. Equivalently, it is the problem of testing whether a given semialgebraic set is non-empty. This decision problem is NP-hard and lies in PSPACE. Thus it has significantly lower complexity than Alfred Tarski's quantifier elimination procedure for deciding statements in the first-order theory of the reals without the restriction to existential quantifiers. However, in practice, general methods for the first-order theory remain the preferred choice for solving these problems.

Many natural problems in geometric graph theory, especially problems of recognizing geometric intersection graphs and straightening the edges of graph drawings with crossings, may be solved by translating them into instances of the existential theory of the reals, and are complete for this theory. The complexity class ${\displaystyle \exists \mathbb {R} }$, which lies between NP and PSPACE, has been defined to describe this class of problems.

...
Wikipedia