CAD-QE on Risa/Asir（使用例）

先のソースコードを cadqe.rr として保存，Asir を起動，それをロードします．

asir -quiet
load("cadqe.rr")$

幾つかのメッセージが表示された後，入力待ちになるので

help("cadqe")$

と入力すると，次のような使用例が表示されます．

cadqe([ex],[a,b,c,x],id,[a*x^2+b*x+c@==0])$
cadqe([all],[a,b,x],imp,[x^2-1@<=0,x^3+a*x+b@<=0])$
cadqe([all,all],[a,b,c,y,x],eq,[a*x^2+b*y^2@<=c,x^2+y^2@<=1])$
def _(A,B,C){and(A,and(B,C));}$cadqe([ex,ex,ex],[a,b,c,x,y,z],_,[x+y+z@==a,x*y+y*z+z*x@==b,x*y*z@==c]|grob=1)$

書式は

cadqe(量化子のリスト,自由変数と束縛変数とのリスト,真理関数または恒等関数id,原子論理式のリスト,オプション)$

ここで，量化子∈{ex,all}，定義済みの真理関数∈{not,and,or,imp,eq}，述語記号∈{@<,@<=,@>,@>=,@==,(@=,)@!=} であり，量化子の個数が n(>0) の場合，変数リストの最後の n 個が各量化子に対する束縛変数です．

例えば

cadqe([ex],[a,b,c,x],id,[a*x^2+b*x+c@==0])$

と入力すると

1[[-oo,[a,1]],[-oo,oo],[[ 4*c*a-b^2 1 ],oo]]
2[[[ a 1 ],[ a 1 ]],[-oo,[b,1]],[-oo,oo]]
3[[[ a 1 ],[ a 1 ]],[[ b 1 ],[ b 1 ]],[[ c 1 ],[ c 1 ]]]
4[[[ a 1 ],[ a 1 ]],[[b,1],oo],[-oo,oo]]
5[[[a,1],oo],[-oo,oo],[-oo,[ 4*c*a-b^2 1 ]]]
0.06575sec + gc : 0.04272sec(0.1256sec)

のように，5個のリストが表示され，各リストはその成分が表す論理式の連言を表し，それらの選言が結果となります．ここで，1個目のリストの第1成分 [-oo,[a,1] ] のリスト [a,1] は a についての多項式 a の小さい方から数えて1個目の実根（つまり，0）の開端点を表し，[-oo,[a,1] ] は -oo

def _(A,B,C){and(A,and(B,C));}$
cadqe([ex,ex,ex],[a,b,c,x,y,z],_,[x+y+z@==a,x*y+y*z+z*x@==b,x*y*z@==c]|grob=1)$

1[[-oo,oo],[-oo,[a^2-3*b,1]],[[ 4*c*a^3-b^2*a^2-18*c*b*a+4*b^3+27*c^2 1 ],[ 4*c*a^3-b^2*a^2-18*c*b*a+4*b^3+27*c^2 2 ]]]
2[[-oo,oo],[[ a^2-3*b 1 ],[ a^2-3*b 1 ]],[[ a^3-27*c 1 ],[ a^3-27*c 1 ]]]
0.2741sec + gc : 0.2713sec(0.5929sec)

直前の projection set は

PP0;

と入力すると

[[],[a^2-3*b],[4*c*a^3-b^2*a^2-18*c*b*a+4*b^3+27*c^2],[x^3-a*x^2+b*x-c,3*x^2-2*a*x-a^2+4*b],[x^2+(y-a)*x+y^2-a*y+b],[x+y+z-a]]
0sec(3.099e-06sec)

のように確認できます（grob=1 オプションなしの場合，この例の projection factors の個数は 200 を超えます）．