QE by full CAD

　まず，前回の a 空間への射影
{ a+3, a, a-1 }
の各多項式の零点 -3，0，1 を境界として，実数全体 R を

(-∞,-3)∪{-3}∪(-3,0)∪{0}∪(0,1)∪{1}∪(1,+∞)

のように，7 個の部分集合に分解し，各部分集合，その式，その要素の一つ(sample point)を組にしたものを，例えば

C(1)=( (-∞,-3),a＜-3,-8 )
C(2)=( {-3},a=-3,-3 )
C(3)=( (-3,0),-3＜a ∧ a＜0,-1 )
C(4)=( {0},a=0,0 )
C(5)=( (0,1),0＜a ∧ a＜1,1/2 )
C(6)=( {1},a=1,1 )
C(7)=( (1,+∞),1＜a,2 )

のように用意します．次に，C(1) に対して，その sample point -8 を射影する前の
A={ x-a, x-a-2, x^2-2*x+a }
の各 a に代入した
{ x+8, x+6, x^2-2*x-8=(x-4)(x+2) }
の各多項式の零点 -8，-6，-2，4 に対応する A の各多項式の零点 a，a+2，r1，r2 を境界として，実数全体 R を

(-∞,a)∪{a}∪(a,a+2)∪{a+2}∪(a+2,s1)∪{r1}∪(r1,r2)∪{r2}∪(r2,+∞)

のように，9 個の部分集合に分解し，各部分集合，その式，a=-8 の場合のその要素の一つ(sample point)を組にしたものを，例えば

C(1,1)=( (-∞,a),x＜a,-9 )
…
C(1,9)=( (r2,+∞),r2＜x,5 )

のように用意します．以下，C(2),...,C(7) に対しても同様にします．
　以上で得られた各組をセル(cell)と呼び，射影の作り方から，各セル上では，A の各多項式が定める関数は常に正，常に0，常に負なので，もとの φ(a,x) ≡ a＜x＜a+2 ∧ x^2-2x+a＜0 の真偽も一定です．従って，2 次元の各セルの sample point を代入するだけで，そのセルの集合上での真偽が判定できます．例えば，C(1,1) に従う sample point a=-8,x=-11 を代入した φ(-8,-11)≡ -8＜-11＜-6 ∧ 108＜0 は偽なので，C(1,1) に従う a＜-3 ∧ x＜a が表す集合上の各点は φ(a,x) を満たしません．
　得られるセルに従う横線集合は R^2 を分割するわけですが，セルの個数は有限なので，上記の真偽判定を全て行えば，R^2 全体を φ(a,x) を満たす部分と満たさない部分とに分けること，つまり，φ(a,x) の解集合をセルの番号の集合で表示できます．

　今回の例では {(3,5),(4,3),(5,5)} がそれであり，これが判れば

∃x (φ(a,x)) の解集合は，C(1),...,C(7)のうち，その上の何れかのセルとの組み合わせで得られる集合が φ(a,x) の解集合に含まれるものの定める集合の和集合
∀x (φ(a,x)) の解集合は，C(1),...,C(7)のうち，その上のセルとの組み合わせで得られる全ての集合が φ(a,x) の解集合に含まれるものの定める集合の和集合

として得ることが出来，今回の例は，∃x (φ(a,x)) なので，その解集合のセル番号の集合は {3,4,5} であり，解集合はそれらのセルの集合の和集合なので，解集合を表す式，すなわち，∃x (φ(a,x)) と等価な式は，セルの式の選言 (0＜a ∧ a＜1)∨(a＝0)∨(-3＜a ∧ a＜0)，つまり，-3＜a＜1 となります．
　なお，RedLog には，セルの個数を出力する rlcadnumauto という関数があり，例えば

rlcadnumauto( ex(x,a < x < a+2 and x^2-2*x+a < 0 ) );
rlcadnumauto( ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1 ) );

に対する出力は，それぞれ 49，32023 です．
　さらに，Maple の RegularChains パッケージの CylindricalAlgebraicDecompose 関数を用いて

CylindricalAlgebraicDecompose(
[x-a,x-a-2,x^2-2*x+a],
PolynomialRing([x,a])
);

とすれば

のように，先の例の 49 個のセルの全てが表示できます．