等価性
nns,nnss と同じく,qex,solvex の入力と出力とは等価,つまり,変数に任意の実数を代入したとき,それらの true,false は一致します.
例えば,sqrt を含む場合,定義:y=sqrt(x)⇔(y^2=x∧y>=0) により,x<0 のとき,y=sqrt(x) は false ですから,前回の最後の例の入力:[ [x^2=a,x>-1] ],出力:[ [a < 1,x = -sqrt(a)],[x = sqrt(a)] ] の等価性は,a<0 のとき入出力とも false,1<=a のとき出力は [ [false],[x = sqrt(a)] ],つまり,[ [x = sqrt(a)] ] といった具合に確かめられますし,xa 座標平面における入力,出力が表す図形が一致することからも判るでしょう.
システム自身に等価性をチェックさせるには,solvex の実行直後に
(%i36) thischeck(); Evaluation took 1.9700 seconds (3.1300 elapsed) using 117.474 MB. (%o36) true
とすればよく,入出力は
(%i37) thisin; Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes. (%o37) (x > -1) %and (x^2 = a) (%i38) thisout; Evaluation took 0.0000 seconds (0.0000 elapsed) using 48 bytes. (%o38) [[a < 1,x = -sqrt(a)],[x = sqrt(a)]]
のように参照出来ます.