Redlog Documentation

documentationrealsrlgqe
rlgqe – generic quantifier elimination

Calling Sequence

rlgqe \((\,\varphi\,)\)
rlgqe \((\,\varphi\,,\ \Theta\,)\)
rlgqe \((\,\varphi\,,\ \Theta\,,\ V\,)\)

Arguments

\(\varphi\) first-order formula
\(\Theta\) list of atomic formulas
\(V\) list of Variables

Returns

\(\{\Theta′,\ \varphi′\}\) \(\{\) list of atomic formulas, first-order formula \(\}\)

Description

Eliminate all quantifiers from \(\varphi\) while globally assuming and collecting in \(\Theta′\) negated equations in the parameters of \(\varphi\) that support the elimination process. In the end, \(\varphi′\) is a quantifier-free equivalent of \(\varphi\) subject to \(\Theta′\). Formally \[ \mathbb{R} \models \bigwedge \Theta′ \longrightarrow (\varphi′ \longleftrightarrow \varphi). \]

When \(\Theta\) is given, then \(\Theta′\supseteq\Theta.\) When \(V\) is given, then rlgqe does not assume any negated equations containing variables from \(V\). However, if such negated equations are already present in \(\Theta\), then those are not removed but occur also in \(\Theta′\). \[ \operatorname{vars}(\Theta'\setminus\Theta)\cap V=\emptyset. \] Furthermore, \(\Theta\) is not limited to negated equations but can contain arbitrary atomic formulas; atomic formulas containing quantified variables will be ignored. Formally In the literature \(\Theta\) and \(\Theta′\) are sometimes called theories, which must not be confused with the theory \(\mathbb{R}\) in which we are computing.

The switch rlqegenct can be turned off to limit the assumptions made by rlgqe to negated equations \(\mu\neq0\), where \(\mu\) is a monomial. Again, non-monomial assumptions already present in \(\Theta\) are not removed but persist.

rlgqe 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 rlgcad.

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 substiutution 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.

Examples

rlgqe ex(x, a*x^2 + b*x + c = 0);

Switches

See Also