Cylindrical Algebraic Decomposition

A recursive projection–lifting algorithm that partitions real n‑space into finitely many cylindrically arranged cells (cells whose projections onto lower dimensions are cells in the decomposition) on which a given finite set of real polynomials has invariant sign, enabling decision procedures for real quantifier and sign queries.