Algorithm Mathematica uses for quantifier elimination procedures

Questions
1

I am a user of SMT. Just switched and testing whether Mathematica can solve inequalities with constraints or not. Surprisingly, It can. But I need to know what procedures and algorithm Mathematica uses for quantifier elimination procedures. Is it the same as Z3, or other SMT tools or not. If not then what is the difference.

Kindly help me with the feedback.
Thanks

2

For real systems, the general algorithm is based on Cylindrical Algebraic Decomposition, but for special cases (e.g. linear or quadratic quantifier elimination) other methods may be used (Weispfenning virtual substitution).

See the documentation for more details and references.