# Redlog Documentation Center

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

rlcad – partial cylindrical algebraic decomposition

## Calling Sequence

rlcad $$(\,\varphi\,)$$

## 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

• 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