###
Introduction
*Mathematica* 4.0 contains several new functions that allow systems of real algebraic equations and inequalities to be solved. In this article we describe the functions, show examples of their use, and comment on the algorithms used in their implementation.
Let us first specify what is meant by a system of algebraic equations and inequalities, and what its solutions are.
An *algebraic expression in variables * is an expression constructed with and rational numbers, using addition, multiplication, rational powers, and the `Root` function. For instance, the following is an algebraic expression in variables *x* and *y*.
A *system of real algebraic equations and inequalities in variables * is a logical combination of equations and inequalities with both sides being algebraic expressions in . For instance, the following is a system of algebraic equations and inequalities in variables *x* and *y*.
Functions that solve systems of real algebraic equations and inequalities always use `LogicalExpand` first to put the system in the disjunctive normal form. For the remainder of this article, we assume that the systems are in the disjunctive normal form; that is, they are disjunctions of conjunctions of equations and inequalities.
A tuple of real numbers *satisfies* (or *is a solution of*) a system of real algebraic equations and inequalities in variables if there is at least one , such that after replacing the with the all the radicals and `Root` objects in are real-valued and all the equations and inequalities in are satisfied.
What does it mean to "solve" a system of real algebraic equations and inequalities? The solutions form *semialgebraic* subsets of . These subsets are often infinite and, unlike complex algebraic sets, cannot be "generically" parametrized using a subset of variables. For instance, the set of solutions of
is the following figure.
In many practical situations (*e.g.,* geometric theorem proving using assumptions), we may need to check very simple properties of systems, like whether a system has any solutions at all, whether a system is always satisfied, or whether the set of solutions of one system is contained in the set of solutions of another system (the first system implies the second). All these problems are equivalent, and we describe functions solving them in the section "Decision Problem."
The set of solutions of any system of real algebraic equations and inequalities in variables can be decomposed into a finite number of "cylindrical" parts.
In the above expression, is one of <, , and ; and and are , , or algebraic expressions in variables which are real-valued for all tuples of real numbers satisfying
In the section "Solving Systems of Equations and Inequalities," we present functions which find solution sets of systems of real algebraic equations and inequalities. We represent these solutions in the *cylindrical solution form*, *i.e.,* in the form of a finite number of disjoint cylindrical parts, with and being `Root` functions, rational functions, or functions of the form for rational functions *a*, *b*, and *c*.
A *quantified system of real algebraic equations and inequalities in variables * is an expression
where is or , and *S* is a system of real algebraic equations and inequalities in .
By Tarski's theorem the solution sets of quantified systems of real algebraic equations and inequalities are semi-algebraic sets. The function `Resolve` , presented in the section "Quantifier Elimination," finds the solution sets and represents them in the cylindrical solution form.
Finally, we show new functions for global optimization of algebraic functions subject to algebraic equation and inequality constraints, and we comment on the algorithms used by the inequality solvers.
Converted by *Mathematica*
April 24, 2000
[Article Index]
[Next Page] |