Re: A problem in mathematical logic

"Bonny Banerjee" <banerjee.28@xxxxxxx> writes:

I am working on a problem that requires eliminating quantifiers from a
logical combination of polynomial equations and inequatlities over the
domain of real numbers, i.e. given a quantified logical expression E, I want
a quantifier-free expression F, such that E and F are equivalent. It has
been shown that the computational complexity of quantifier elimination is
inherently doubly exponential in the number of variables. I want to know
whether quantifier elimination can be done in lesser time if we take the
help of examples.

I've heard of the doubly exponential result (Monk?). But sometimes doubly
exponential results are misleading in the sense that the problems that come
up in actual practice tend to run quickly. I don't know whether that applies
to the elimination of quantifiers for real closed fields.

Anyway, one thing you might do is try out some particular examples and see
how much time and space they really take up, as compared with the double
exponential that is the worst case scenario.

For example, Jack Schwartz had a paper on robot motion planning in which
he used the decision procedure for real closed fields. In practice, people
do get robots to move and to solve motion problems.
--
Ignorantly,
Allan Adler <ara@xxxxxxxxxxxxxxxxxxxx>
* Disclaimer: I am a guest and *not* a member of the MIT CSAIL. My actions and
* comments do not reflect in any way on MIT. Also, I am nowhere near Boston.
.