RSolver
今回は以前 http://d.hatena.ne.jp/ehito/20110526/1306382983 少し述べた numeric QE プログラム，RSolver http://rsolver.sourceforge.net/ について書きます．
一般に QE とは，与えられた論理式と等価で，量化子を含まない論理式を得る処理のことですが，今のところ作動原理から，扱えるのは代数関数に限られます．これに対して numeric QE は，結果を論理式ではなく，論理式（及びその否定）が定める解集合の区間塊による近似に留める代わりに，初等超越関数まで扱えるようにしたもののことです．
では，いつものようにインストールスクリプトです（なお，現ヴァージョンは64bit専用です）．
mkdir ~/CAS cd ~/CAS wget http://jaist.dl.sourceforge.net/project/rsolver/rsolver/rsolver_3.1.tar.gz tar zxvf ./rsolver_3.1.tar.gz cd ./rsolver sudo ln -s ./rsolver /usr/local/bin/rsolver
実行ファイルは，rsolver 本体とそのGUIスクリプト rsolver-gui.sh ですが，後者はカレントのファイルを呼ぶのでインストール先に移動してから
cd ~/CAS/rsolver ./rsolver-gui.sh
とすることになります．起動すると
のように初期状態で既にサンプルが入力されていますので，そのまま Submit をクリックすれば
が現れます．この図は自由変数の空間の Domain で指定した部分であり，その緑色の部分は Constraint（論理式）が T となる範囲の部分集合，赤色の部分は F となる範囲の部分集合を表し，右の一覧からそれらを構成する box（区間の直積）が読み取れ，上に並んだボタンやマウスによる範囲指定で，描画範囲を狭くすると，Domain も変更されるので，改めて Submit をクリックすれば，より細かな情報が得られます．
ただし，Results ウインドウが落ちたり，プロセスが残ったりするので GUI はお勧めできません．また，図が現れるのは自由変数の個数が 0,1,2 のときだけです．
入力の書式は
[自由変数の列] 論理式; [自由変数の閉区間の列]
であり，記号は
Quantifiers:
FORALL, EXISTS
Connectives:
\/, /\, ==>
Predicates:
<, <=, >, >=
Function Symbols:
*, +, SIN, COS, EXP, ASIN, ACOS, ATAN, LOG
Constants:
floating point numbers, PI, E
Variables:
lowercase alphanumeric strings starting with a letter
例えば，接線の掃引範囲は
[x,y] EXISTS[s][[0,2]] [y=EXP(s)*(x-s+1)]; [[-2.0,4.0],[-1.0,5.0]]
といった具合です．例は，/examples 以下にあります．
なお，rsolver 本体をそのまま起動すると対話形式になってしまうので
cat 入力ファイル名 | rsolver
または
echo -e "入力ファイルの中身" | rsolver
とするのが簡便です．rsolver -h で表示されるオプションのうち
結果を逐次表示させる -i volume（長さ，面積，体積，…）が X の区間まで計算させる -e X
は基本かと思います．
以下は，指定した集合に含まれる円板の半径の長さの条件です．
echo "[r]
EXISTS[a,b][[0,1],[0,1]]
FORALL[x,y][[0,1],[0,1]]
[(x-a)^2+(y-b)^2<r^2 ==> [0<y /\ y<COS(0.5*PI*x) /\ 0<x /\ x<1]];
[[0.34,0.36]]" | rsolver -i -e 0.001
==================================================================
RSolver 3.1
by
Stefan Ratschan
Czech Academy of Sciences
with
Peter Franek, Tomas Dzetkulic, Sven Buente, Varadarajulu Reddy Pyda
includes:
smathlib by Timothy Hickey and David Wittenberg
==================================================================
Variables (not quantified): Constraint: Box: F: r in [ 0.3575, 0.36]
F: r in [ 0.355, 0.3575]
F: r in [ 0.354350024644, 0.355]
F: r in [ 0.353425012322, 0.354350024644]
F: r in [ 0.35125, 0.3525]
T: r in [ 0.34, 0.34125]
T: r in [ 0.34125, 0.3425]
T: r in [ 0.3425, 0.34375]
F: r in [ 0.3525, 0.353425012322]
F: r in [ 0.350625, 0.35125]
F: r in [ 0.35, 0.350625]
F: r in [ 0.349375, 0.35]
T: r in [ 0.34375, 0.344375]
T: r in [ 0.345, 0.345625]
T: r in [ 0.345625, 0.34625]
T: r in [ 0.344375, 0.345]
F: r in [ 0.349281875456, 0.349375]
F: r in [ 0.348125, 0.34875]
F: r in [ 0.34875, 0.349281875456]
F: r in [ 0.3478125, 0.348125]
F: r in [ 0.3475, 0.3478125]
T: r in [ 0.34625, 0.3465625]
T: r in [ 0.3465625, 0.346875]
F: r in [ 0.347484565845, 0.3475]
T: r in [ 0.346875, 0.34703125]
T: r in [ 0.34703125, 0.347109375]
F: r in [ 0.34734375, 0.347484565845]
T: r in [ 0.347109375, 0.347155693225]
F: r in [ 0.347331139078, 0.34734375]
F: r in [ 0.347316199373, 0.347331139078]
F: r in [ 0.347265625, 0.347316199373]
F: r in [ 0.347251849686, 0.347265625]
F: r in [ 0.3472265625, 0.347251849686]
T: r in [ 0.3471875, 0.34720703125]
T: r in [ 0.347171596612, 0.3471875]
T: r in [ 0.347155693225, 0.347171596612]
True, volume ~[ 0.00720703125, 0.00720703125]
r in [ 0.347155693225, 0.347171596612]
r in [ 0.347171596612, 0.3471875]
r in [ 0.3471875, 0.34720703125]
r in [ 0.347109375, 0.347155693225]
r in [ 0.34703125, 0.347109375]
r in [ 0.346875, 0.34703125]
r in [ 0.3465625, 0.346875]
r in [ 0.34625, 0.3465625]
r in [ 0.344375, 0.345]
r in [ 0.345625, 0.34625]
r in [ 0.345, 0.345625]
r in [ 0.34375, 0.344375]
r in [ 0.3425, 0.34375]
r in [ 0.34125, 0.3425]
r in [ 0.34, 0.34125]
False, volume ~[ 0.0127734375, 0.0127734375]
r in [ 0.3472265625, 0.347251849686]
r in [ 0.347251849686, 0.347265625]
r in [ 0.347265625, 0.347316199373]
r in [ 0.347316199373, 0.347331139078]
r in [ 0.347331139078, 0.34734375]
r in [ 0.34734375, 0.347484565845]
r in [ 0.347484565845, 0.3475]
r in [ 0.3475, 0.3478125]
r in [ 0.3478125, 0.348125]
r in [ 0.34875, 0.349281875456]
r in [ 0.348125, 0.34875]
r in [ 0.349281875456, 0.349375]
r in [ 0.349375, 0.35]
r in [ 0.35, 0.350625]
r in [ 0.350625, 0.35125]
r in [ 0.3525, 0.353425012322]
r in [ 0.35125, 0.3525]
r in [ 0.353425012322, 0.354350024644]
r in [ 0.354350024644, 0.355]
r in [ 0.355, 0.3575]
r in [ 0.3575, 0.36]
Unknown:
r in [ 0.34720703125, 0.347216796875]
r in [ 0.347216796875, 0.3472265625]
これにより，上限は [ 0.34720703125, 0.3472265625] に属することが解ります．
