![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
QEPCAD B v1.69 is a program for studying Cylindrical Algebraic Decomposition (CAD). It constructs CADs from an input formula and variable order, and provides many commands for getting info out of the CAD, including construction of simple equivalent Tarski formulas.
Quantifier Elimination (入力された論理式と等価で，量化子を含まない論理式を出力する) プログラムの定番です．
MathLibre (20130831) ではインストール済みです．それ以前のバージョンでは次を実行してください．
sudo apt-get -y install bison flex export CAS=/usr/local/CAS export qe=$CAS/qesource export saclib=$CAS/saclib2.2.5 sudo mkdir $CAS sudo chmod 777 $CAS cd $CAS wget http://www.usna.edu/cs/~qepcad/INSTALL/saclib2.2.5.tar.gz tar zxvf ./saclib2.2.5.tar.gz cd $saclib/bin ./sconf ./mkproto ./mkmake ./mklib all cd $CAS wget http://www.usna.edu/cs/~qepcad/INSTALL/qepcad-B.1.69.tar.gz tar zxvf ./qepcad-B.1.69.tar.gz cd $qe sed -i "s/csh/sh/g" $qe/Makefile make sed -i "s/\#SINGULAR/SINGULAR/g" $qe/default.qepcadrc cd $CAS wget http://www.usna.edu/cs/~qepcad/SLFQ/simplify-1.20.tar.gz tar zxvf simplify-1.20.tar.gz cd ./simplify make echo "export qe=/usr/local/CAS/qesource" >> ~/.bashrc sudo ln -s $CAS/qesource/bin/qepcad /usr/local/bin/qepcad sudo ln -s $CAS/simplify/slfq /usr/local/bin/slfq
円と直線
echo "[] (a,b,x,y) 2 (Ex)(Ey)[x^2+y^2<=1 /\ a x+b y=1]. finish" | qepcad
オプション
echo "[] (a,b,x,y) 2 (Ex)(Ey)[x^4+y^3<=1 /\ a x+b y=1]. finish" | qepcad +N2000000 +L10000
x->aのときのx^3の極限
echo "[] (a,b,p,q,x) 2 (Ap)(Eq)(Ax)[[p <= 0 \/ [q > 0 /\ [[ - x - q + a >= 0 \/ x - q - a >= 0] \/ [ - x^3 - p + b < 0 /\ x^3 - p - b < 0]]]]]. finish" | qepcad
「QEPCAD」パッケージをロードすると，REDUCE 上から Redlog の書式で QEPCAD B が利用できます．ただし，MathLibre (20130831) の REDUCE は最小の構成なので，パッケージが呼ぶスクリプトファイルをビルドされた時の場所に置く必要があります．次を実行してください．
export bap=/build/build-reduce-algebra_20110414-1~getdeb2-amd64-XKpkL0/reduce-algebra-20110414/packages/redlog/qepcad sudo mkdir -p $bap sudo wget http://sourceforge.net/p/reduce-algebra/code/HEAD/tree/trunk/packages/redlog/qepcad/qepcad.awk?format=raw -O $bap/qepcad.awk
なお，空きスペースに余裕のある場合，REDUCE の項に従いフル構成にアップグレードすれば，この処理は不要です．
REDUCE をターミナル，白黒モードで起動
reduce -w -b
パッケージのロード
load qepcad;
QEPCAD の利用
on rlnzden,rladdcond;
rlqepcad ex({x,y},y=1/x and a*x+b*y=1);
slfq の利用
on rlslfqvb;
rlqe ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1);
rlslfq ws;
オプション
rlqepcadn 50000000;
rlqepcad ex({x,y,z},x^2+y^2+z^2=1 and a*x+b*y+c*z=1);
終了
quit;
:included in knxm:
