## Calling Sequence

## Arguments

\(\varphi\) | — | first-order formula |

## Returns

\(\varphi′\) | — | quantifier-free formula, or the original formula in case of failure |

## Description

Eliminate quantifiers from \(\varphi\) using cylindrical algebraic decomposition. The result is a quantifier-free formula \(\varphi′\) that is equivalent to \(\varphi\). Formally, \[ \mathbb{R} \models \varphi′ \longleftrightarrow \varphi. \] Unless one is interested in particularly applying CAD as a method, it is recommended to use rlqe instead, which implicitly calls rlcad on suitable subproblems when necessary.

The implementation of rlcad follows the standard scheme with three phases: projection, lifting, and formula construction.

Up to three remaining variables the projection phase uses McCallum's projection operator. For higher dimensions it uses Hong's projection. For generally using Hong's projection turn on the switch rlcadmc3. The projection processes quantifier blocks from the inside to the outside, followed by the parameters. Within each block established heuristics are used to determine the variable order.

The lifting phase uses partial cylindrical algebraic decomposition for pruning
the CAD tree. Furthermore, it employs incremental root isolation and eager
truth value evaluation. It generally uses exact arithmetic. The experimental
switch rlcadtree2dot can be turned on to dump the
resulting partial CAD tree for visualization. This generates files
`cadtree.dot`

`cadtree.tgf`

, and
`cadtree.gml`

in `/tmp`

. The directory can be changed in
the variable `ofsf_wd!*`

. In particular, ```
lisp(ofsf_wd!* :=
"./");
```

will select the current working directory. Note that existing
files with the above names will be overwritten.

The formula construction phase uses Simple Solution Formula Construction (SSFC) to compute a quantifier-free formula from the partial CAD tree. In rare cases SSFC can fail. Currently, there is no augmented projection available to recover from such failures, and the original input formula \(\varphi\) is returned.

## Examples

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

rlcad all(x, ex(y, x^2 + x*y + b > 0 and x + a*y^2 + b <= 0));

rlcad all(x, x^4 + p*x^2 + q*x + r >= 0);

## Switches

⊕ = on by default, ⊖ = off by default- rlcadmc3
^{⊕}— McCallum's projection for dimension two and three - rlcadtree2dot
^{⊖}— dump the resulting partial CAD tree into a file

## See Also

- 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
- rlqepcad — file system-based interface to QEPCAD B
- rlqews — quantifier elimination with selection

## References

- G. E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. LNCS 33, 1975.
- G. E. Collins and H. Hong. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. J. Symb. Comput. 12(3), 1991.
- A. Dolzmann, A. Seidl, and T. Sturm. Efficient projection orders for CAD. Proc. ISSAC 2004.
- H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. Proc. ISSAC 1990.
- H. Hong. Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination. Proc. ISSAC 1992.
- S. McCallum. An improved projection operation for cylindrical algebraic decomposition of three-dimensional space. J. Symb. Comput. 5(1-2), 1988.
- A. Seidl. Cylindrical Decomposition Under Application-Oriented Paradigms. PhD thesis, Universität Passau, Germany, 2006.