Message Boards

5032 Views

1 Reply

4 Total Likes

View groups...

Follow this post

Share this post:

GROUPS:

Mathematics Mathematica Wolfram Language

Algorithm Mathematica uses for quantifier elimination procedures

Posted 12 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

1 Reply

Sort By:

Posted 12 years ago

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

Reply Preview

Attachments

Remove Add a file to this post

Follow this discussion

or Discard

Feedback