Message Boards Message Boards

1 Reply
4 Total Likes
View groups...
Share this post:

Algorithm Mathematica uses for quantifier elimination procedures

Posted 11 years ago
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.
POSTED BY: Usman Rauf
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.
POSTED BY: Ilian Gachevski
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract