Question: Do you know an effective Gröbner's method over the reals?

I would like to use Gröbner's method to study polynomial systems (with equality or (and) inequalities) in the case where the variables are REAL. It is known that in general the problem is much more complicated than in the complex case; in particular it is necessary to use gradient methods.
In Maple, we can use the patch "Raglib" (Lip6 laboratory). However "with (RAG)" does not work very well, even for "simple problems" like this one: the $ 9 $ real unknowns are $ X = [x_ {i, j}] \ in M_3 (\ mathbb {R} $. The  system to satify is $ X ^ TX = I_3, x [1,1] <1 / 2,3 / 10 <x [2,3] $, that is, $6$ polynomial equations and $2$ inequalities; clearly, a particular solution is a permutation of the canonical basis. The "HasRealSolutions" command does not provide any result after 2 hours 15 minutes of calculation. The "PointsPerComponents" command indicates that there are no solutions... 
It seems to me that we can also use "RegularChains" but I am not familiar with this library.

  Have you any ideas on these questions? Thank you in advance.
 
Please Wait...