MathGroup Archive 2006

[Date Index] [Thread Index] [Author Index]

Search the Archive

A problem in mathematical logic

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.

Suppose I have a quantified logical expression E1 and its equivalent 
quantifier-free expression F1. Now I am given another quantified logical 
expression E2 and the task is to compute its equivalent quantifier-free 
expression, say F2. Instead of spending a lot of time computing F2 from E2 
using the quatifier elimination algorithm, I want to know whether there 
exists a mapping between E2 and E1, so that F2 can be computed from F1 by 
reverse-mapping. This idea will be beneficial only if there exists such a 
mapping that can be computed in time less than doubly exponential.

Example of a mapping: If I can show that E1 and E2 are equivalent, then F1 
and F2 have to be equivalent. So "equivalence" is an example of such a 
mapping. Unfortunately, the general problem of equivalence checking is 

I suspect, there might exist a mapping weaker than equivalence (and 
computable in polynomial time) that will suffice for my purposes. Please let 
me know if any of you are already aware of any such mapping. Any suggestion 
regarding which book/paper to look at would also help.

Thanks much,

  • Prev by Date: RE: Please help overcome problems with integration
  • Next by Date: Re: Definite integrals in Mathematica
  • Previous by thread: Re: Missing <<Miscellaneous`PhysicalConstants` package
  • Next by thread: Re: A problem in mathematical logic