Redlog Documentation Center

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

documentationrealsrlcad

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

See Also

References

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