Théorie existentielle sur les réels

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 the variables are interpreted as having real number values, and where is a quantifier-free formula involving equalities and inequalities of real polynomials. A sentence of this form is true if it is possible to find values for all of the variables that, when substituted into formula , make it become true. The decision problem for the existential theory of the reals is the problem of finding an algorithm that decides, for each such sentence, 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, giving it 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. The complexity class has been defined to describe the class of computational problems that may be translated into equivalent sentences of this form. In structural complexity theory, it lies between NP and PSPACE. Many natural problems in geometric graph theory, especially problems of recognizing geometric intersection graphs and straightening the edges of graph drawings with crossings, belong to , and are complete for this class. Here, completeness means that there exists a translation in the reverse direction, from an arbitrary sentence over the reals into an equivalent instance of the given problem. In mathematical logic, a theory is a formal language consisting of a set of sentences written using a fixed set of symbols.