The RegularChains:-SemiAlgebraicSetTools subpackage contains a collection of commands for manipulating semi-algebraic systems and their solution sets. A semi-algebraic system is a set of equations, inequations and inequalities given by polynomials; the coefficients of those polynomials and the unknowns are all real numbers. A solution of such system is a point whose coordinates satisfy all these equations, inequations and inequalities simultaneously once the coordinates of this point replace the polynomial variables, according to a prescribed variable ordering.

The RegularChains library offers a rich set of tools for manipulating semi-algebraic systems and their solutions. A large portion of those commands are located in the RegularChains:-SemiAlgebraicSetTools subpackage. Others can be found in the RegularChains:-ParametricSystemTools subpackage, such as RealRootClassification and RealComprehensiveTriangularize or at the top-level of the library, such as RealTriangularize, SamplePoints, LazyRealTriangularize.

For semi-algebraic systems with finitely many solutions, the RegularChains:-SemiAlgebraicSetTools subpackage provides commands for isolating and counting the solutions of such systems. These commands can also be used for isolating and counting the real roots of zero-dimensional regular chains (that is, regular chains with a finite number of complex solutions).

Each real root of a zero-dimensional regular chain (or of a semi-algebraic system with finitely many solutions) can be isolated using a so-called box, that is, a Cartesian product of singletons and open intervals. See the commands RealRootIsolate and BoxValues.

Each box can be refined with an arbitrary small precision. See the commands RefineBox and RefineListBox.

Two methods can be used for isolating real roots of zero-dimensional regular chains and semi-algebraic systems. The first one is a generalization of the Vincent-Collins-Akritas Algorithm which isolates real roots for univariate polynomials. The techniques are very close to the ones used by Renaud Rioboo in his ISSAC 1992 paper (see reference below). The other method implements the algorithm of the paper "An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems." by B. Xia and L. Yang.

The command RealRootCounting counts the number of solutions of a semi-algebraic system with finitely many solutions.

The empty set is a special semi-algebraic set which can be constructed by the command EmptySemiAlgebraicSet.

An important tool provided by this package is a command for cylindrical algebraic decomposition. See the command CylindricalAlgebraicDecompose. In broad terms, for a given set of polynomials in n variables, this commands computes a partition of the n-dimensional Euclidean space into regions, where the sign (negative, null or positive) of each of those polynomials does not change.

Another related tool is a command for partial cylindrical algebraic decomposition. See the command PartialCylindricalAlgebraicDecomposition. It computes only the maximal dimensional cells of the cylindrical algebraic decomposition induced by the input polynomials and represent each of which by a rational sample point. It can be used as a subroutine to decide whether a semi-algebraic system with only strict positive inequalities has solutions or not. Together with the other commands of this package, it is an essential tool for studying the real solutions of polynomial systems, with or without parameters. For the parametric case, see the command RealRootClassification. For the non-parametric case, see the command RealTriangularize.

The output of RealTriangularize is a list of regular semi-algebraic systems. A regular semi-algebraic system is the adaptation of the notion of a regular chain to the purpose of computing the real solutions of a polynomial system, by means of triangular decomposition techniques. See the mathematical definitions below and the command RealTriangularize for details.

Another important command is QuantifierElimination, which returns a quantifier-free logic formula logically equivalent to the quantified formula given as input.

The command RemoveRedundantComponents returns a list of regular semi-algebraic system whose zero sets are pairwise noninclusive.  The input and output regular semi-algebraic systems should have the same zero set.

The output of RealRootClassification is a pair consisting of a list of regular semi-algebraic sets and a so-called border polynomial. Up to exceptional cases, a border polynomial is a list of polynomials. See the mathematical definitions below and the command BorderPolynomial for details.

The commands Complement, Difference, Intersection, IsEmpty, IsContained and Projection perform operations on semi-algebraic sets represented by regular semi-algebraic systems.

The commands RepresentingBox, IsParametricBox, DisplayParametricBox, LinearSolve, RepresentingChain, PositiveInequalities, RepresentingQuantifierFreeFormula, DisplayQuantifierFreeFormula, RepresentingRootIndex, VariableOrdering can be used to inspect regular semi-algebraic systems and regular semi-algebraic sets.

A regular semi-algebraic system of R is the data of a regular chain rc of R, a list P of polynomials of R (each of them defining a positive inequality) and a quantifier-free formula Q given by polynomials involving the free variables of rc only. In addition, the following three constraints are satisfied. First, each polynomial in P is regular w.r.t. the saturated ideal of rc. Second, Q defines a non-empty and open semi-algebraic set C in the space of the free variables of rc. Third, if $S$ denotes the semi-algebraic system whose equations are given by the polynomials of rc, whose positive inequalities are given by the polynomials of P and with no inequations, then $S$ admits real solutions at any point of C.

The zero set of the regular semi-algebraic system given by rc, P and Q consists of all the zeros of $S$ that extend a point of  C.

A regular semi-algebraic set is an encoding for some (or all the) real solutions of a regular chain rc whose non-algebraic variables are constrained in a non-empty semi-algebraic set C such that rc separates well (that is, is delineable) and admits a positive constant number of real solutions at any point of C.

In theory, a regular semi-algebraic set can always be defined as the union of zero sets of finitely many regular semi-algebraic systems and vice versa. However, the first encoding is more suitable for certain algorithms such as the one of the RealRootClassification command. This encoding is described below.

When it is finite, a regular semi-algebraic set can be encoded as a list of points with real coordinates. Each point is defined by a regular chain and a Cartesian product of isolation intervals. Such an encoding is called a numeric box (or simply a box). See the commands RealRootIsolate and BoxValues for more precise details.

When it is infinite, a regular semi-algebraic set can be encoded by the data of a regular chain rc of R, a quantifier-free formula Q given by polynomials involving the free variables of rc and a root index list L (to be defined hereafter). In addition, the two following properties must hold. The quantifier-free formula Q  defines a non-empty semi-algebraic set C such that rc separates well (that is, is delineable) and admits a positive and constant number of real solutions at any point of C. As a consequence, you can index the real solutions of rc uniformly above C. This is where root index list L is introduced. It allows one to select some of the real roots of rc. Finally, the regular chain rc, the quantifier-free formula Q and the root index list L form a so-called parametric box.

A square-free semi-algebraic system of R is a square-free regular system (as defined in ConstructibleSetTools) given by a regular chain rc of R and a polynomial set P such that each polynomial in P must be regular modulo the saturated ideal of  rc, which itself must be radical. The zero set of this square-free semi-algebraic system consists of the real points of the quasi-component of rc which make each polynomial in P strictly positive. The type squarefree_semi_algebraic_system is used for square-free semi-algebraic systems.

A semi-algebraic set is any zero set of a semi-algebraic system. Here semi-algebraic system is understood as any finite disjunction of conjunction of polynomial equations, inequations and inequalities. The type semi_algebraic_set is used for semi-algebraic sets. One  possible representation is by regular semi-algebraic systems. An alternative representation is by CAD cells.

A CAD cell of the n-dimensional Euclidean space with coordinates x1 < ... < xn is defined recursively as follows. For n=1 it is either a point or an interval; in the first case x1 is set to an algebraic expression while in the second case x1 is strictly bounded between two algebraic expressions; in both cases each of these algebraic expressions is a RootOf expression where the defining polynomial is univariate over the rational numbers. For n>1 it is a CAD cell of the n-1-dimensional space together with a constraint on xn of type section or sector. In the first case xn is set to an algebraic expression and in the second xn is strictly bounded between two algebraic expressions; in both cases, each algebraic expression is a RootOf expression where the defining polynomial is univariate with coefficients that are polynomials in the previous coordinates.

The following is a list of the available commands.

Changbo Chen, Marc Moreno Maza "An Incremental Algorithm for Computing Cylindrical Algebraic Decomposition." Proceedings of ASCM 2012, Computer Mathematics, Springer, (2014): 199-221.

Changbo Chen, Marc Moreno Maza "Quantifier elimination by cylindrical algebraic decomposition based on regular chain." J. Symb. Comput. 75: 74-93 (2016)

Changbo Chen, Marc Moreno Maza "Simplification of Cylindrical Algebraic Formula." Computer Algebra in Scientific Computing (CASC), Lecture Notes in Computer Science - 9301, (2015): 119-134.

F. Boulier, C. Chen, F. Lemaire, M. Moreno Maza "Real root isolation of regular chains." ASCM'09, Math-for-Industry,  Lecture Note Series Vol. 22 (2009): 15-29.

C. Chen, J.H. Davenport, J. May, M. Moreno Maza, B. Xia, R. Xiao, Y. Xie "User interface design for geometrical decomposition algorithms in Maple." MathUI'09.

C. Chen, J.H. Davenport, J. May, M. Moreno Maza, B. Xia, R. Xiao "Triangular Decomposition of semi-algebraic systems." ISSAC'10, ACM Press, 2010.

C. Chen, J.H. Davenport, M. Moreno Maza, B. Xia, R. Xiao "Computing with semi-algebraic sets represented by triangular decomposition". ISSAC'11, ACM Press, 2011.

C. Chen, M. Moreno Maza, B. Xia, L. Yang "Computing cylindrical algebraic decomposition via triangular decomposition." ISSAC'09, ACM Press, 2009.

C. Chen, and M. Moreno Maza. "Semi-algebraic description of the equilibria of dynamical systems." Proc. Cof the 2011 International Workshop on Computer Algebra in Scientific Computing  (CASC 2011),  LNCS Vol. 6885: 101-125. Springer, 2011.

R. Rioboo. "Computation of the real closure of an ordered field." ISSAC'92, Academic Press, San Francisco.

L. Yang, X. Hou, B. Xia. "A complete algorithm for automated discovering of a class of inequality-type theorems." Sci. China Ser. F, Vol. 44 (2001): 33-49.

B. Xia, L. Yang. "An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems." J. Symb. Comput., Vol. 34 No. 5 (2002): 461-477.