F1 (formula 5.14 from the article) = (A a)(A b)(A c2)[ [0 <= a <= 1 /\ 0 <= b <= 1] ==> A <= 0 /\ C <= 0 /\ [D <= 0 \/ B <= 0] ]where A, B, C, and D are polynomials in a,b, and c2.
A = c2^4 (a - b + 1) ( a - b - 1) (a - b)^2 B = 2 c2^4 b ( 3 a^2 b - 2 a^2 - 2 a b^2 + a + b^3 - b) + 4 c2^3 a b ( a^2 - a + b^2 - b) + 2 c2^2 a ( a^3 - 2 a^2b + 3 a b^2 - a - 2 b^2 + b ) C = c2^4 b^2 (b^2 - 1) + 4 c2^3 a b^2 (b - 1) + 2 c2^2 a b (3 a b - 2 a - 2 b + 1) + 4 c2 a^2 b (a - 1) + a^2 (a^2 - 1) D = c2^2 ( 8 a^2 b^2 - 12 a^2 b + 5 a^2 - 8 a b^3 + 8 a b^2 + 2 a b - 4 a + 4 b^4 - 4 b^3 - 3 b^2 + 4 b ) + 2 c2 ( 4 a^3 b - 2 a^3 - 4 a^2 b^2 - 2 a^2 b + a^2 + 4 a b^3 - 2 a b^2 + 2 a b - 2 b^3 + b^2 ) + 4 a^4 - 8 a^3 b - 4 a^3 + 8 a^2 b^2 + 8 a^2 b - 3 a^2 - 12 a b^2 + 2 a b + 4 a + 5 b^2 - 4 b
Gfor "generic" in QEPCAD B) and produce an equivalent formula. QEPCAD B is able to return "true" for this formulation in about 2 seconds on my 800Mhz P3 laptop. See the QEPCADB input.
The moral of the story is this: "for all but finitely many" can be decided using CAD faster than "for all" (which makes sense, since finitely many points can be ignored), so you should use it if you can. Note, however, that it doesn't make a difference with the top-level quantifier.
A <= 0 /\ C <= 0 /\ [D <= 0 \/ B <= 0] ]onto the a-b plane looks like. So here it is (the unit grid is shown in green, and the coordinate axes in red) at least up to some lower dimensional subset. It's a bizarre picture when you think about it. These polynomials just happen to intersect along a couple of planes that are nicely algined with the coordinate axes.
Here only one quantifier was eliminated, so the
G quantifier doesn't help us. However,
QEPCAD B is able to compute adjacencies between cells in a CAD
of 2-space, and has a command called
(which stands for "truth value closure 2D") that completes truth
value assignments to cells of a CAD of 2-space based on the
assumption that the solution set is the closure of an open set,
which should be the case for this problem. So, I instructed
QEPCADB to lift over cells in 2-space only when they had full
dimension, and used tvc2d to assign truth values to the lower
dimensional cells. See the