DISCOVERER

　前回紹介した RealRootClassification および
RegularChains[ParametricSystemTools][BorderPolynomial],
RegularChains[ParametricSystemTools][DiscriminantSequence],
RegularChains[SemiAlgebraicSetTools][RealRootIsolate] with method='Discoverer'
といった関数群は，DISCOVERER （http://www.is.pku.edu.cn/~xbc/discoverer.html）という外部パッケージを取り込んだもので，使用上の注意さえ心得ていれば，汎用の QE ツールにはない軽快さを体感できます．
　その注意とは次の２つです．

　注意１
入力するのは，少なくとも1個の方程式とパラメータ（自由変数）を含み，パラメータの殆ど全ての値に対して，解集合が有限集合となるシステム（0 dimensional system）

つまり，システムの実数解の「個数」を指定し，そのためのパラメータの条件を求めるツールであるということです．なお，RealRootClassification のオリジナルである DISCOVERER の tofind 関数は，少なくとも1個の方程式と未知数（束縛変数）を含むなら入力可能で，パラメータを含まないシステム（constant system）も処理できるのですが，Maple としては，他にも関数があるので，parametric system に専念させたいようです．

　注意２
付加された前提以外の場合については，その場合のシステムを改めて入力する

つまり，場合分け毎に入力が必要ということです．
　それでは

with(RegularChains):
with(ParametricSystemTools):
infolevel[RegularChains]:=1:

のように，パッケージをロード，メッセージの出力レベルを設定して，上記に注意しながら，前回の例を再度処理してみましょう．まずは
∃x ( x^2=a )
ですが

RealRootClassification([x^2-a] , , , [] , 1 , 1..n , PolynomialRing([x,a]) ):

と入力すると

RealRootClassification: FINAL RESULT:
RealRootClassification: The system has given number of real solution(s) IF AND ONLY IF
RealRootClassification: [0 < R[1] ]
RealRootClassification: where
RealRootClassification: R[1] = a
RealRootClassification: PROVIDED THAT
RealRootClassification: a <> 0
RealRootClassification: 0.

つまり
（１）a≠0 のときは，a＞0
と答えますので，注意２により，a＝0 のときのシステムを

RealRootClassification([x^2-a,a] , , , [] , 1 , 1..n ,
PolynomialRing([x,a]) ):

のように与えてみると

RealRootClassification: The number of solutions is 1.
RealRootClassification: There is(are) 1 parametric point(s) satisfying the condition(s).
RealRootClassification: The system has real solution(s) at 1 of those parametric points.
RealRootClassification: The solutions are grouped according to the parameters as follows:
RealRootClassification: [{[[0, 0], [0, 0] ] } ]
RealRootClassification: "boxes NewAll:" [ { [ [0, 0], [0, 0] ] }, [1, [a] ] ]
RealRootClassification: "There is no parameters and the system is 0 dimensional!"

つまり
（２）a＝0 のときは丁度1個の解をもつ
と答えますので，（１）または（２）とすれば，a≧0 が得られます．
　前回２つ目の例は
∃x ∃y ( x^2+y^2=1 ∧ x+y≧a )
でした．しかし，a＜sqrt(2) のとき，このシステムの解は，円弧上に無限に存在しますので，注意１に反してしまいます．では，どうするか？ すぐに思い付くのは，この条件を
∃b (∃x ∃y ( x^2+y^2=1 ∧ x+y=b ) ∧ b≧a )
と変形し，内側の b についての条件を利用する方法です．実際

RealRootClassification([x^2+y^2-1,x+y-b],[ ],[ ],[ ],1,1..n,PolynomialRing([x,y,b])):

と入力すると

RealRootClassification: FINAL RESULT:
RealRootClassification: The system has given number of real solution(s) IF AND ONLY IF
RealRootClassification: [R[1] < 0]
RealRootClassification: where
RealRootClassification: R[1] = b^2-2
RealRootClassification: PROVIDED THAT
RealRootClassification: b^2-2 <> 0
RealRootClassification: 0.

そして，注意２により

RealRootClassification([b^2-2,x^2+y^2-1,x+y-b],[ ],[ ],[ ],1,1..n,PolynomialRing([x,y,b])):

と続ければ

RealRootClassification: The number of solutions is 2.
RealRootClassification: There is(are) 2 parametric point(s) satisfying the condition(s).
RealRootClassification: The system has real solution(s) at 2 of those parametric points.
RealRootClassification: The solutions are grouped according to the parameters as follows:
RealRootClassification: [{[[-2, -1], [-1, -1/2], [-3/2, 0] ] }, {[[5/4, 3/2], [5/8, 3/4], [1/2, 7/8] ] } ]
RealRootClassification: "boxes NewAll:" [{[[-2, -1], [-1, -1/2], [-3/2, 0] ] }, {[[5/4, 3/2], [5/8, 3/4], [1/2, 7/8] ] }, [1, [b^2-2] ] ]
RealRootClassification: "There is no parameters and the system is 0 dimensional!"

と出力され

∃x ∃y ( x^2+y^2=1 ∧ x+y=b ) ≡ b^2-2≦0 ≡ -sqrt(2)≦b≦sqrt(2)

と判り，a≦sqrt(2) が得られます．
　以上の例では，やはり一般の QE ツールの方が便利ですが，例えば，以前扱った
円周 (x-a)^2+(y-b)^2=c^2 が集合 x^2＜y＜x に含まれるための条件
はどうでしょう？かなり乱暴ですが

RealRootClassification([(x-a)^2+(y-b)^2-c^2,(y-x^2)*(y-x)],[ ],[ ],
[ ],3,0,PolynomialRing([x,y,a,b,c])):

と入力すると，10秒ほどで

RealRootClassification: FINAL RESULT:
RealRootClassification: The system has given number of real solution(s) IF AND ONLY IF
RealRootClassification: [0 < R[1], 0 <= R[3], 0 < R[4] ]
RealRootClassification: OR
RealRootClassification: [0 < R[1], 0 <= R[2], R[3] <= 0, 0 < R[4] ]
RealRootClassification: where
RealRootClassification: R[1] = a^2-2*a*b+b^2-2*c^2
RealRootClassification: R[2] = 4*a^2-4*c^2+4*b-1
RealRootClassification: R[3] = 8*a^2*b-8*b*c^2+14*a^2+8*b^2+4*c^2-6*b+1
RealRootClassification: R[4] = 16*a^6+16*a^4*b^2-48*a^4*c^2-32*a^2*b^2*c^2+48*a^2*c^4+16*b^2*c^4-16*c^6-40*a^4*b-32*a^2*b^3+8*a^2*b*c^2-32*b^3*c^2+32*b*c^4+a^4+32*a^2*b^2-20*a^2*c^2+16*b^4-8*b^2*c^2-8*c^4-2*a^2*b-8*b^3+8*b*c^2+b^2-c^2
RealRootClassification: PROVIDED THAT
RealRootClassification: a <> 0
RealRootClassification: a^2+b^2-c^2 <> 0
RealRootClassification: a^2+b^2-c^2-2*a-2*b+2 <> 0
RealRootClassification: a^2-2*a*b+b^2-2*c^2 <> 0
RealRootClassification: 25*a^4-40*a^3*b+26*a^2*b^2-10*a^2*c^2-8*a*b^3+8*a*b*c^2+b^4-2*b^2*c^2+c^4-2*a^3-18*a^2*b+14*a*b^2-14*a*c^2-2*b^3+2*b*c^2+2*a^2+2*b^2-2*c^2 <> 0
RealRootClassification: 16*a^6+16*a^4*b^2-48*a^4*c^2-32*a^2*b^2*c^2+48*a^2*c^4+16*b^2*c^4-16*c^6-40*a^4*b-32*a^2*b^3+8*a^2*b*c^2-32*b^3*c^2+32*b*c^4+a^4+32*a^2*b^2-20*a^2*c^2+16*b^4-8*b^2*c^2-8*c^4-2*a^2*b-8*b^3+8*b*c^2+b^2-c^2 <> 0

と返ってくるので，Mathematica に

ans := Or[And[0 < R[1], 0 <= R[3], 0 < R[4] ],
And[0 < R[1], 0 <= R[2], R[3] <= 0, 0 < R[4] ] ];
R[1] = a^2 - 2*a*b + b^2 - 2*c^2;
R[2] = 4*a^2 - 4*c^2 + 4*b - 1;
R[3] = 8*a^2*b - 8*b*c^2 + 14*a^2 + 8*b^2 + 4*c^2 - 6*b + 1;
R[4] = 16*a^6 + 16*a^4*b^2 - 48*a^4*c^2 - 32*a^2*b^2*c^2 + 48*a^2*c^4 + 16*b^2*c^4 - 16*c^6 - 40*a^4*b - 32*a^2*b^3 + 8*a^2*b*c^2 - 32*b^3*c^2 + 32*b*c^4 + a^4 + 32*a^2*b^2 - 20*a^2*c^2 + 16*b^4 - 8*b^2*c^2 - 8*c^4 - *a^2*b - 8*b^3 + 8*b*c^2 + b^2 - c^2;
Reduce[Exists[{a, b}, a^2 < b < a, ans && c > 0], Reals]

と尋ねてみると，確かに

0 < c < 1/(8 Sqrt[2])

となっています．