# Redlog Documentation Center

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

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
• rlqestdans — computation of standard answers for formulas without parameters

• rlgcad   —   generic partial cylindrical algebraic decomposition
• rlhqe   —   Hermitian quantifier elimination
• rllqe   —   local quantifier elimination
• rlmma   —   file system-based interface to real QE in Mathematica
• rlposqe   —   positive quantifier elimination
• rlqe   —   quantifier elimination
• rlqeipo   —   quantifier elimination in position