Projection Phase

　これまでの考察により

　F(a,x) が a(∈R^n),x(∈R) についての実係数多項式 f_j(a,x) (j=1,...,M) を左辺，0 を右辺とする方程式や不等式を ∧ や ∨ で結合した論理式のとき
　∃x F(a,x) や ∃x F(a,x)
を満たす a 全体の集合を a についての実係数多項式 g_i(a) (i=1,...,N) を左辺，0 を右辺とする方程式や不等式を ∧ や ∨ で結合した論理式で表す際の g_i の候補には，各 f_j(a,x) を束縛変数 x についての多項式と見たとき
（０）自由変数のみを含むもの
（１）自由変数を含む，主係数とそれに続く係数
（２）異なる多項式の定数でない終結式
（３）見かけの次数が 2 以上の多項式の定数でない判別式
がある

ことが判りました．
　以下では，一般に多項式の空でない有限集合 A に対して，A に属する各多項式の既約因数から（０），（１），（２），（３）のいずれかとして得られる多項式の既約因数全体の集合を A の自由変数空間への射影，あるいは，A の束縛変数方向の射影と呼ぶことにします．例えば，
{ x-a, x-a+2, x^2-2*x+a }
に対して，（０），（１）はなく，（２）は
\|\array{1&-a\\1&-a+2}\|=2
\|\array{1&-a&0\\0&1&-a\\1&-2&a}\|=a^2-a=a(a-1)
\|\array{1&-a+2&0\\0&1&-a+2\\1&-2&a}\|=a^2+3a=a(a+3)
（３）は，(x^2-2*x+a)'=2(x-1) により
\|\array{1&-2&a\\1&-1&0\\0&1&-1}\|=a-1
なので，a 空間への射影は
{ a+3, a, a-1 }
です．
　（０）〜（３）以外の候補については，ひとまず保留し，次回，これらを用いた QE を一般にも通用する形でお話したいと思います．
　なお，RedLog には，この処理のための関数 rlcadproj があり

rlcadproj ( a

と入力すれば

{ {a + x**2 - 2*x, - a + x - 2, - a + x},
{a,a - 1,a + 3} }

と答えてくれます．