Message Boards Message Boards

2
|
4525 Views
|
1 Reply
|
4 Total Likes
View groups...
Share
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.
Thanks
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
Attachments
Remove
or Discard

Group Abstract Group Abstract