MathGroup Archive 2006

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

Search the Archive

Re: A problem in mathematical logic

  • To: mathgroup at smc.vnet.net
  • Subject: [mg72268] Re: [mg72242] A problem in mathematical logic
  • From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
  • Date: Sun, 17 Dec 2006 06:20:24 -0500 (EST)
  • References: <200612161017.FAA12165@smc.vnet.net>

On 16 Dec 2006, at 19:17, Bonny Banerjee wrote:

> 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.

Not quite true. The Basu, Pollack, Roy algorithm is double  
exponential in the number of blocks of variables, where the blocks  
are delimited by alternations of the existential and universal  
quantifiers. This means you need to have at least two blocks and at  
lest on of them must have more than one variable, for this to make a  
difference.


> 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
> NP-hard.
>
> 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.
>

Each of yoru two expressions E1 and E2 is equivalent to specifying  
some semi-algebraic set. I have not given much thought to your  
question, but at this time the only way I can imagine of constructing  
(in the general case) your mapping is by using Cylindrical  
Decomposition, which is indeed inherently double exponential  
(although there are approximate versions which are only single  
exponential - e.g. Experimental`GenericCylindricalDecomposition` ).  
The improvements in complexity of a number of algorithms (such as  
computing the connected components of a semi-algebraic set,   
quantifier elimination etc.) achieved by Basu, Pollack and Roy is due  
to their being able to avoid the need to use Cylindrical  
Decomposition. The relevant book is
"Algorithms in Real Algebraic Geometry" by Basu, Pollack and Roy  
(Springer, Algorithms and Computation in mathematics, Volume 10).  
(However, this book has 580 pages and the relevant algorithms are all  
near the end).

Andrzej Kozlowski




  • Prev by Date: RE: Re: Combinatorica parameters
  • Next by Date: system of nonlinear equations in mathematica?
  • Previous by thread: A problem in mathematical logic
  • Next by thread: Re: A problem in mathematical logic