Décomposition Algébrique Cylindrique

Une procédure récursive de projection‑relevage qui partitionne l'espace réel de dimension n en un nombre fini de cellules disposées de façon cylindrique (les projections d'une cellule sont des cellules de la décomposition) sur lesquelles un ensemble fini de polynômes réels a un signe invariant, permettant de décider des requêtes de signe et d'éliminer des quantificateurs réels.