Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentationrealsrlqea

rlqea – quantifier elimination with answer

Calling Sequence

rlqea \((\,\exists x_n \dots \exists x_1\psi\,)\)

Arguments

\(\varphi\) first-order formula of the form \exists x_n \dots \exists x_1\psi

Returns

\(EQR;\) extended quantifier elimination result

Description

Eliminate quantifiers from \(\varphi\) to obtain an extended quantifier elimination result (EQR) of the form \[ \left[ \begin{array}{c|ccc} \beta_1(\mathbf{u}) & x_1=e_{11}(\mathbf{u}) & \dots & x_n=e_{1n}(\mathbf{u})\\ \vdots & \vdots & \ddots & \vdots\\ \beta_k(\mathbf{u}) & x_1=e_{k1}(\mathbf{u}) & \dots & x_n=e_{kn}(\mathbf{u}) \end{array} \right]. \] The conditions \(\beta_i(\mathbf{u})\) are quantifier-free formulas in the parameters \(\mathbf{u} = (u_1,\dots,u_m)\). The answers \(e_{ij}(\mathbf{u})\) are terms in an extension of the Tarski language. The returned EQR has the following semantics:

  1. The disjunction of the conditions \(\beta_i(\mathbf{u})\) is a quantifier-free equivalent of \(\varphi\). Formally, \[ \mathbb{R} \models \bigvee_{i=1}^{k} \beta_i(\mathbf{u}) \longleftrightarrow \varphi. \]
  2. For every \(\beta_i(\mathbf{u})\) we obtain an answer \(e_{ij}(\mathbf{u})\) for the existentially quantified variable \(x_j\), i.e., for any choice \(\mathbf{a}\in\mathbb{R}^m\) of the parameters \(\mathbf{u} = (u_1,\dots,u_m)\) the following holds: If \(\mathbf{a}\) satisfies \(\beta_i\), then \(e_{i1}(\mathbf{a}),\dots,e_{in}(\mathbf{a})\) describe real choices for the variables \(x_1,\dots,x_n\) that satisfy \(\psi\). Formally, \[ \mathbb{R} \models \beta_i(\mathbf{a}) \quad \text{implies} \quad \mathbb{R} \models \psi(e_{i1}(\mathbf{a}), \dots, e_{in}(\mathbf{a})). \]

Note that if \(\exists x_n \dots \exists x_1\psi\) is equivalent to false, then the empty EQR \([\quad]\) is possibly returned.

If the quantifier elimination procedure fails, then the input formula \(\exists x_n \dots \exists x_1\psi\) is returned.

If the outermost block of quantifiers in \(\varphi\) is not an existential block, then the output of rlqea is undefined.

Examples

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

Switches

⊕ = on by default, ⊖ = off by default

See Also

References

  1. V. Weispfenning. Quantifier elimination for real algebra—The quadratic case and beyond. Appl. Algebr. Eng. Comm. 8(2):85–101, 1997.