# Two questions on strategies for quantifier elimination

With the help of people here I was able to solve several cases similar to IC3 but this case - unlike the other cases - does not return an answer. I will try to run it for a day with 8 processors but will be grateful for:

1. Any suggestions on how to solve IC3 (besides more memory or more time)
2. In the end I only care about some other constraints so would help resolve if I add additional constraints on the other variables (a, c and d) when trying to eliminate x and z?

IC3 := (4 d^3 + 24 a d^2 x + 3 (2 a + c) d (-c x^2 + 2 a (x^2 + 4 x z - 2 z^2)) - (2 a + c)^2 (c x^3 + 4 a (x^3 - 3 x^2 z + z^3)))/(6 (2 a + c)^2)
&& 0 < -((2 d)/(2 a + c)) < 1
Resolve[{x,z}, (-(2 d)/(2 a + c)) <= x <= 1, (-d/(2 a + c))<=z<=(-(2 d)/(2 a + c)), IC3]

-

This is not an answer but my guess what is going wrong. Feel free to edit it.

My guess is that Mathematica has problems when the solution is lower dimensional and/or empty.

The polynomial inequality described by IC3 can be expressed as F[x,z] >=0 for some F function. Say we find the region of parameters {a,b,c} such that it holds true for all x and for z == -d/(2 a + c)) or z == -2d/(2 a + c)). That is, for z at the boundary, we have a region of {a,b,c} where the inequality is true. If the inequality where to reverse for an interior z then the derivative with respect to z must be zero, D[F[x,z],z]==0, the second derivative must be non-negative (local-minimum), D[F[x,z],z,z]>=0.

If we try to solve D[F[x,z],z]==0 and D[F[x,z],z,z]>0 in the region where x and z are, we get an empty solution. If we try to solve D[F[x,z],z]==0 and D[F[x,z],z,z]==0 we get some solutions where a==0 (i.e. a lower dimensional set)

-