Computer algebra systems that can handle real-closed fields? I'm trying to solve a big system of:
quadratic equations with coefficients in $\mathbb{Z}$, each in 6 variables,
quadratic inequalities with coefficients in $\mathbb{Z}$, each in 6 variables, and
linear inequalities of the form $x_i>0$.
There are on the order of a couple of dozen equations in my system.  I know that the system has exactly one solution in the real numbers, and the solution is algebraic.  Some of the equations might be extraneous.
I don't know anything about the solution space over $\mathbb{C}$ or over the entire field of algebraic numbers.  Presumably there are more solutions there, though I don't know this for sure, either.
I need an exact solution, so for every variable, I want either a closed expression for it, or an irreducible polynomial in one variable that has it as a root.
I've looked into MAGMA for this, hoping to solve the system using a computer algebra implementation of Groebner bases.  However, I am having a couple of problems.
My questions are:


*

*How might I include the inequalities in my system?  Is there a way to make them into equalities?  I don't mind introducing extra variables.

*Is there a computer algebra system that will find Groebner bases over the real algebraic numbers?  Or, is this something I could possibly implement with a little work from existing solvers that work over the algebraic closure of $\mathbb{Q}$?
 A: Not really useful enough for an answer, but a little long to be a comment:
While it is true that you can introduce extra variables and constrain their squares to be the quantities which you wish to be nonnegative, these "nonnegativity" constraints don't really buy you anything when you look at them over an algebraically closed field like C.  You may be introducing lots of new solutions and it will not necessarily be easy to pick out your unique real solution from an algebraic description of all of these.  You could just as well drop the nonnegativity constraints and look at which complex solutions are real and happen to satisfy the inequalities; that is essentially what this approach amounts to.  For this reason Groebner bases and such are not really suited to problems in real closed fields where the order plays a big role (of course there are no doubt times when one can still get valuable information by looking at the equations over C).
Nonetheless there are algorithms that will do what you're looking for in theory: look up terms like quantifier elimination and cylindrical algebraic decomposition.  There is software implementing such algorithms such as QEPCAD which is freely available.  But beware, the computational complexity of quantifier elimination is horrible and such algorithms are extremely slow and memory intensive in practice.  For a problem of the size you state though, it may be worth a shot.
A: Let me expand a bit on Noah's answer: first, you do not want to add those extra slack variables: the number of variables is the worst parameter (doubly exponential!) in the complexity of cylindrical algebraic decomposition. And the algorithm is built to handle inequalities anyway.
Most computer algebra systems will have implementations of cylindrical algebraic decomposition. Some will even have the more sophisticated critical point method first programmed by Safey El Din. As Noah pointed out, these algorithms are very taxing and any flaw in the implementation renders them essentially useless, so you might have to seek a specialized package like QEPCAD.
The good news is that many researchers in the area are eager to know the kind of practical problems that people are really interested in (there's nothing like a real problem to benchmark your experimental algorithms). If your problem is too challenging for off-the-shelf solutions yet still tractable, they might be able to help. If you could give a better idea of what the system looks like (or better yet post it), we can find out if it looks solvable or not.
A: Can you include slack variables to turn the inequalities into equalities?
Also, I think that you'll have to use the algebraic closure of Q, since of course you can only represent numbers in Q or in Q multiplied by sqrts, symbolically in the second case.
There's a book called "Algorithms in Real Algebraic Geometry" that might house the answer, unfortunately I don't have it with me at the moment.
