title: Théorie existentielle sur les réels
text: # 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 $\exists \mathbb {R}$, pour laquelle des problèmes géométriques sur les graphes sont $complets^,.$
  
  ## Problèmes $\exists \mathbb {R}$-complets
  
  La classe $\exists \mathbb {R}$ 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 $\exists \mathbb {R}$-dur si tout problème de $\exists \mathbb {R}$ s'y réduit en temps polynomial. Un problème est $\exists \mathbb {R}$-complet s'il est dans $\exists \mathbb {R}$ et s'il est $\exists \mathbb {R}$-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 $\exists \mathbb {R}$-complet.
  
  