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.

[Article Index] [Next Page]