拡張タルスキー論理式
今回はQEPCAD Bの特徴の一つである，Extended Tarski Formulas（http://www.usna.edu/CS/~qepcad/B/user/ETF.html）についてお話しましょう．入力は，以前書いたバッチ処理と同じ書式ですが，ファイルは作らずecho出力をパイプ処理で読み込ませます．例えば
echo -e "[] \n (a,b,x,y) \n 2 \n (Ex)(Ey)[x^2+y^2=1 /\ a x+b y=1]. \n finish" | qepcad
といった具合です．
さて表題の論理式ですが，これは一つの変数と一つの方程式の一つの根との相等，大小関係を表すもので，例えばx=sqrt(5)という条件を用いる際，これはタルスキー論理式（有理係数の多項式の方程式，不等式）ではないのでQEPCAD Bに入力することはできず，x^2=5 /\ x>0 等と次数を上げて入力することになりますが，QEPCAD Bは次数や変数の個数の増加に対して非常にデリケートですので，あまり良い手段とは言えません．拡張タルスキー論理式はこの点を改善するものであり
x=_root_2 x^2-5
がx=sqrt(5)と同値なそれです．書式は
変数 等号または不等号 _root_0以外の整数 その変数についての有理係数の定数以外の多項式
であり，式の右辺は，0以外の整数が
正の整数nのとき，与えられた多項式の，正の向きに数えてn番目の実根，
負の整数-nのとき，与えられた多項式の，負の向きに数えてn番目の実根
を表し，nが多項式の相異なる実根の個数より大きいときは，式自体がFALSE，一般には
∃r(r=(n番目の実根)∧変数 等号または不等号 r)
と同値になります．従って
x=_root_-2 x^2-5，x=_root_-1 x^2-5，x=_root_1 x^2-5，x=_root_2 x^2-5，x=_root_3 x^2-5，
はそれぞれ
x=-sqrt(5)，x=sqrt(5)，x=-sqrt(5)，x=sqrt(5)，FALSE
と同値であり
knoppix@Microknoppix:~$ echo -e " \n (x,a,b,c) \n 1 \n (Ea)(Eb)(Ec)[x=a+b+c /\ a=_root_1 a^3-3 a+1 /\ b=_root_2 b^3-3 b+1 /\ c=_root_3 c^3-3 c+1]. \n finish" | qepcad
=======================================================
Enter an informal description between '[' and ']':Enter a variable list:
(x,a,b,c)Enter the number of free variables:
1
Enter a prenex formula:
(Ea)(Eb)(Ec)[x=a+b+c /\ a=_root_1 a^3-3 a+1 /\ b=_root_2 b^3-3 b+1 /\ c=_root_3 c^3-3 c+1].=======================================================
Before Normalization >
finishAn equivalent quantifier-free formula:
x = 0
といった具合です．
また，QEPCAD Bの出力はデフォルトではタルスキー論理式を用いますので，根が書き下せない場合の表現を見るのも一興です．
knoppix@Microknoppix:~$ echo -e " \n (x) \n 1 \nx=_root_5(x-1)(x-2)(x-3)(x-4)(x-5)-1. \n finish" | qepcad
=======================================================
Enter an informal description between '[' and ']':Enter a variable list:
(x)Enter the number of free variables:
1
Enter a prenex formula:
x=_root_5(x-1)(x-2)(x-3)(x-4)(x-5)-1.=======================================================
Before Normalization >
finishAn equivalent quantifier-free formula:
2 x^2 - 12 x + 15 > 0 /\ x - 3 > 0 /\ x^5 - 15 x^4 + 85 x^3 - 225 x^2 + 274 x - 121 = 0
なお，多項式が1変数，つまり，根が定数のときは，負の整数を与える必要は認められませんが，多変数の場合は，係数によって相異なる実根の個数が変わるので，境界の含み方となって違いが現れます．例えば
y=_root_2 x^2+y^2-5
y=_root_1 x^2+y^2-5
y=_root_-1 x^2+y^2-5
y=_root_-2 x^2+y^2-5
はそれぞれ
y > 0 /\ y^2 + x^2 - 5 = 0 （相異なる実根が２個あるのはこの範囲のみ）
y <= 0 /\ y^2 + x^2 - 5 = 0
y >= 0 /\ y^2 + x^2 - 5 = 0
y < 0 /\ y^2 + x^2 - 5 = 0 （相異なる実根が２個あるのはこの範囲のみ）
と同値であり，例えば，半円周x^2+y^2=1，y<0と直線x+y=cとに共有点が存在するという条件なら
knoppix@Microknoppix:~$ echo -e " \n (c,x,y) \n 1 \n (Ex)(Ey)[y=_root_-2 x^2+y^2-1 /\ x+y=c]. \n finish" | qepcad
=======================================================
Enter an informal description between '[' and ']':Enter a variable list:
(c,x,y)Enter the number of free variables:
1
Enter a prenex formula:
(Ex)(Ey)[y=_root_-2 x^2+y^2-1 /\ x+y=c].=======================================================
Before Normalization >
finishAn equivalent quantifier-free formula:
c^2 - 2 <= 0 /\ c - 1 < 0
といった具合です．
これに対して，出力に拡張タルスキー論理式の利用を許すには，Before Solutionフェーズでsolution-extension Eと入力すると，例えば
knoppix@Microknoppix:~$ echo -e " \n (c,x,y) \n 1 \n (Ex)(Ey)[y=_root_-2 x^2+y^2-5 /\ x+y=c]. \n go \n go \n go \n solution-extension E \n finish" | qepcad
=======================================================
Enter an informal description between '[' and ']':Enter a variable list:
(c,x,y)Enter the number of free variables:
1
Enter a prenex formula:
(Ex)(Ey)[y=_root_-2 x^2+y^2-5 /\ x+y=c].=======================================================
Before Normalization >
goBefore Projection (y) >
goBefore Choice >
goBefore Solution >
solution-extension E
An equivalent quantifier-free formula:c^2 - 10 <= 0 /\ c < _root_-1 c^2 - 5
Before Solution >
finishAn equivalent quantifier-free formula:
c^2 - 10 <= 0 /\ [ c^2 - 5 < 0 \/ c < 0 ]
のようになります．
多変数の場合の注意点として，変数vについての拡張タルスキー論理式では，その右辺の多項式に含まれるv以外の変数は，Enter a variable list: においてvに先立って入力したもの（その変数空間の分解がvより後のもの）でなくてはなりません．従って
echo -e "[] \n (c,x,y) \n 1 \n (Ex)(Ey)[x=_root_-2 x^2+y^2-3 /\ x+y=c]. \n finish" | qepcad
としようものなら
(Ex)(Ey)[x=_root_-2 x^2+y^2-3 /Not a *proper* Extended Tarski Formula!
と叱られます．
