Eliminate all quantifiers from \(\varphi\) so that \(\varphi'\) is a quantifier-free equivalent of \(\varphi\). Formally, \[ \mathbb{R} \models \varphi' \longleftrightarrow \varphi. \]

When \(\Theta\) is given, the elimination result is correct for all interpretations of the parameters in \(\varphi\) that satisfy \(\Theta\). Formally, \[ \mathbb{R} \models \bigwedge \Theta \longrightarrow (\varphi' \longleftrightarrow \varphi). \] In the literature \(\Theta\) is sometimes called a theory, which must not be confused with the theory \(\mathbb{R}\) in which we are computing.

rlqe combines two quantifier elimination methods: virtual substitution and partial cylindrical algebraic decomposition (CAD).

The implementation of virtual substitution is limited to quantifiers, where the degree of the quantified variable does not exceed 2. A quantified variable is called linear when it is not multiplied with other quantified variables, in particular not with itself. With the elimination of a nonlinear quantified variable the degrees of the other variables possibly increase. On the other hand, degrees are decreased during elimination by various heuristic simplification techniques. If at some point during elimination all remaining quantifiers exceed the degree bound of 2, then virtual substitution cannot continue. This is called a degree violation. Unless in the input formula all quantified variables are linear, it cannot be excluded that there will be degree violations.

In case of degree violation, rlqe switches to CAD for the remaining quantifiers. This application of CAD can be prohibited by turning off the switch rlqefb. Note that then the result \(\varphi'\) is not necessarily quantifier-free. For directly applying partial CAD use the function rlcad.

For the elimination of a block of like quantifiers, virtual substitution applies a variable selection strategy. The switch rlqevarsel can be turned off for instead eliminating the quantifiers in the given order (from the inside to the outside).

For a more exhaustive search for a good elimination order the switch rlqevarseltry can be turned on. This significantly slows down virtual substitution but might be the key to get through virtual substitution without degree violations.

The switch rlqegsd can be turned on to compute for the elimination of each existential quantifier block a DNF and distribute the existential quantifiers over the top-level disjunction. Furthermore, this DNF is simplified using Gröbner basis methods. Blocks of universal quantifiers are treated analogously.

The switches rlqeqsc and rlqesqsc can be turned on to optimize elimination set computation for variables occurring with degree 2 so that an increase of the degree of other quantified variables can be avoided in special cases. This leads to larger results in general but might prevent degree violations.