Théorie existentielle sur les réels

En logique mathématique, la théorie existentielle sur les réels est l'ensemble des formules existentielles de la logique premier ordre vraies sur les réels. Elle est intéressante pour la planification de mouvement de robots. Elle est décidable et NP-dure et dans PSPACE. Elle définit aussi une classe de complexité entre NP et PSPACE, notée $\mathrm{\exists }ℝ$, pour laquelle des problèmes géométriques sur les graphes sont completsModèle:,.

Problèmes $\mathrm{\exists }ℝ$-complets

La classe $\mathrm{\exists }ℝ$ est la classe des problèmes de décision qui se réduisent en temps polynomial à vérifier si une formule de la théorie existentielle sur les réels est vraie. Un problème est $\mathrm{\exists }ℝ$-dur si tout problème de $\mathrm{\exists }ℝ$ s'y réduit en temps polynomial. Un problème est $\mathrm{\exists }ℝ$-complet s'il est dans $\mathrm{\exists }ℝ$ et s'il est $\mathrm{\exists }ℝ$-dur.

Le problème de savoir si un graphe non orienté peut être dessiné dans le plan en représentant les arêtes par des lignes droites de longueur 1 est $\mathrm{\exists }ℝ$-complet.