cineqs4 原理

cineqs4 は「真理値に関する中間値定理」により,原始式同士の結合の様子に立ち入ることなく,系を解いています.すなわち,...
一変数半代数系 F(x) と実数 a,b (a,<,>=,<=,=,#}) について,{rel(f(a),0),rel(f(b),0)}={true,false}
例えば,f(a)>0はtrue,f(b)>0はfales(つまり,f(b)<=0はtrue)なので
⇒F(x) のある原始式 rel(f(x),0) (rel∈{>,<,>=,<=,=,#}) について,f(c)=0,a<=c<=b となる実数 c がある
という性質(つまり,連続関数 f の零点に触れなければ F の真理値は変わらないこと)により,系に現れるすべての f のすべての相異なる実数の零点 n (>=0) 個とその間,および,両脇との合計 2n+1 個の代表点についての F の真理値は,各点,各区間における真理値に一致するので,true となった代表点に対する点,区間を表す式の選言が解集合の式となる訳です.

具体例です.

(%i1) ep(1,0)$cineqs4('(   ((x-1)*(x^2-3)<=0 and x>0) or x^2-x-1=0   ));
Evaluation took 0.0000 seconds (0.0000 elapsed) using 856 bytes.
Evaluation took 0.0800 seconds (0.0800 elapsed) using 2.356 MB.
(%o2) [[x = -(sqrt(5)-1)/2],[1 <= x,x <= sqrt(3)]]

処理の様子は,コントローラー ep (algExact and Print) の第二引数を 1 にすれば確認できます.

(%i3) ep(1,1)$cineqs4('(   ((x-1)*(x^2-3)<=0 and x>0) or x^2-x-1=0   ));
Evaluation took 0.0000 seconds (0.0000 elapsed) using 992 bytes.
((x-1)*(x^2-3) Lc2 0) and (x Go 0) or (x^2-x-1 Eq 0) 
((x-1)*(x^2-3) Lc2 0) and (x Go 0) or (x^2-x-1 Eq 0) 
[((x-1)*(x^2-3) Lc2 0) and (x Go 0) or (x^2-x-1 Eq 0),{}] 
[[-sqrt(3),-(sqrt(5)-1)/2,0,1,(sqrt(5)+1)/2,sqrt(3)],
 ((x-1)*(x^2-3) Lc2 0) and (x Go 0) or (x^2-x-1 Eq 0)]
  
[[((-2*sqrt(3))-1)/2,-sqrt(3),((-(sqrt(5)-1)/2)-sqrt(3))/2,-(sqrt(5)-1)/2,
  -(sqrt(5)-1)/4,0,1/2,1,((sqrt(5)+1)/2+1)/2,(sqrt(5)+1)/2,
  ((sqrt(5)+1)/2+sqrt(3))/2,sqrt(3),(2*sqrt(3)+1)/2],
 [false,false,false,true,false,false,false,true,true,true,true,true,false]]
  
Evaluation took 0.0300 seconds (0.0400 elapsed) using 2.036 MB.
(%o4) [[x = -(sqrt(5)-1)/2],[1 <= x,x <= sqrt(3)]]

この例では多項式なので最初の3行はあまり変化しません(Lc2 は less close,Go は greater open,Eq は equal).

次の [-sqrt(3),-(sqrt(5)-1)/2,0,1,(sqrt(5)+1)/2,sqrt(3)] が (x-1)*(x^2-3),x,x^2-x-1 の零点 6 個であり,最後に表示されたリストが,上で述べた代表点 13 個と対応する ((x-1)*(x^2-3) Lc2 0) and (x Go 0) or (x^2-x-1 Eq 0) の真理値です.

その結果において,左から 4 番目が true なので [x = -(sqrt(5)-1)/2],8から12番目までがtrue なので [1 <= x,x <= sqrt(3)],他は false,ということで,(%o4) が得られます.