Maple の動向（その３） - ATPとCASのこと

　Maple 10 で登場した ChainTools パッケージに， Maple 14 で追加されたサブパッケージ SemiAlgebraicSetTools の目玉が，以前出力をご覧頂いた CylindricalAlgebraicDecompose です．
　この関数は，全空間を与えられた有限個の多項式関数の符号を変えない部分集合に分割する，いわゆる full CAD を実行するもので，その結果をセルの式とsample pointの範囲のリストとして出力します．
　使い方は，まず

with(RegularChains):
with(ChainTools):
with(SemiAlgebraicSetTools):

のようにパッケージをロードすれば，後は

CylindricalAlgebraicDecompose([多項式の列],PolynomialRing([束縛変数，自由変数の列]));

とするだけです．なお，変数の消去（射影）は，PolynomialRing の左側の変数から順に行われます（Mathematica の CylindricalDecomposition とは逆順です）．
　例えば，a*x+b に従う (a,b,x) 空間の分割（x，b，a の順に消去）は

CylindricalAlgebraicDecompose([a*x+b],PolynomialRing([x,b,a]));

と入力すれば

のよう 9 個のセルの式とsample pointの範囲が出力され，(b,a,x) 空間の分割（x，a，b の順に消去）は

CylindricalAlgebraicDecompose([a*x+b],PolynomialRing([x,a,b]));

と入力すれば

のようになり，21 個のセルの式とsample pointの範囲が出力されます．
　この結果があれば，先に述べた特称量化，全称量化の幾何学的な特徴付けにより
∃x ( a*x+b=0 )，∀x ( a*x+b＞0 )
といった式が QE できます．例えば，上の 21 個のセルを用いて，∃x ( a*x+b=0 ) を QE するなら

cad:=CylindricalAlgebraicDecompose([a*x+b],PolynomialRing([x,a,b]),output=list):
for k from 1 to nops(cad) do
if
is(subs(b=cad[k][2][2][1][1],a=cad[k][2][2][2][1],x=cad[k][2][2][3][1],a*x+b=0))
then print(cad[k]) fi od;

と入力し

[ [ 1, 1, 2], [regular_chain, [ [ -1, -1], [-1, -1], [-1, -1] ] ] ]

[ [ 1, 3, 2], [regular_chain, [ [ -1, -1], [1, 1], [1, 1] ] ] ]

[ [ 2, 1, 2], [regular_chain, [ [ 0, 0], [-1, -1], [0, 0] ] ] ]

[ [ 2, 2, 1], [regular_chain, [ [ 0, 0], [0, 0], [0, 0] ] ] ]

[ [ 2, 3, 2], [regular_chain, [ [ 0, 0], [1, 1], [0, 0] ] ] ]

[ [ 3, 1, 2], [regular_chain, [ [ 1, 1], [-1, -1], [1, 1] ] ] ]

[ [ 3, 3, 2], [regular_chain, [ [ 1, 1], [1, 1], [-1, -1] ] ] ]

のように a*x+b=0 を満たすsample pointをもつセルをリストアップ（第1成分はセルのインデックスで，例えば，[ 3, 1, 2 ] の式は，0

[1, 1]　から　b<0,a<0
[1, 3]　から　b<0,a>0
[2, 1]　から　b=0,a<0
[2, 2]　から　b=0,a=0
[2, 3]　から　b=0,a>0
[3, 1]　から　b>0,a<0
[3, 3]　から　b>0,a>0

の選言をとれば

Or(And(b<0,a<>0),b=0,And(b>0,a<>0))

が得られます．
　この CylindricalAlgebraicDecompose は，まず押さえるべき QE の手段である full CAD の実装に他ならず，これまで裏？からのアプローチに留まっていた Maple がようやく正面から QE と向き合う覚悟を持った証のようにも見えます．かつて，Mathematica 4 が実験的に QE 関連の関数を導入し，瞬く間に QEPCAD ＆ RedLog という最強コンビを追い越したように，Maple の一層の注力と進展に期待しています．