maxima で QE（その１） 決定問題と最適化問題

　今回は，CAD は一回お休みして，いきなり始まった「 maxima で QE 」シリーズの１をお送りします．
　以下では，∀x P(x) や ∃x P(x) (x∈R^N) のような量化子の種類が 1 で，しかも，自由変数を含まない論理式（閉論理式）を扱います．
　閉論理式の真偽を判定することは一般に決定問題と呼ばれますが，上記の閉論理式の真偽判定には，ある種の関数の下限の符号が判れば十分だというのが，今回のお話です．
　扱う P(x) はこれまで同様，x についての実数係数の連続関数で表された不等式と等式を原始論理式とする量化子を含まない論理式なのですが，等式 A＝0 は A≧0 ∧ A≦0 と等価ですので，連言標準形，および，全称量化子の連言に対する分配可能性により，∀x P(x) は

（１）　∀x ( A_1(x)≧0 ∨ … ∨ A_m(x)≧0 ∨ B_1(x)＞0 ∨ … ∨ B_n(x)＞0 )

の形としてよく，さらに

　∃x P(x)≡¬( ∀x( ¬( P(x) ) ) )

なので，∀x P(x) のみを考えればよいことになります．
　で，（１）の真偽判定の方法ですが，素朴に

　（１）
⇔ どのような実数 x に対しても，m 個の値 A_1(x)，…，A_m(x) のうち少なくとも 1 つは 0 以上，または，n 個の値 B_1(x)，…，B_n(x) のうち少なくとも 1 つは正
⇔ どのような実数 x に対しても，max{ A_1(x)，…，A_m(x) } ≧ 0 または max{ B_1(x)，…，B_n(x) } ＞ 0
⇔ どのような実数 x に対しても，max{ B_1(x)，…，B_n(x) } ≦ 0 ならば max{ A_1(x)，…，A_m(x) } ≧ 0
⇔ inf_{max{ B_1(x)，…，B_n(x) } ≦ 0}( max{ A_1，…，A_m } )(x) ≧ 0

と言い変えれば

max 関数の下限の符号判定

に帰することが判ります．例えば
∀x ∀y ∀z ( x^2+y^2+z^2≦1 → (x+y+z)^2≦3 )
は
inf_{ x^2+y^2+z^2≦1 } ( 3-(x+y+z)^2 ) ≧ 0
と等価であり，maxima でその真偽を見るなら，線形近似ですが，非線形制約の最適化問題（最適化問題 - Wikipedia）solver である cobyla により

load(fmin_cobyla)$
fmin_cobyla( 3-(x+y+z)^2 , [x,y,z] , [0,0,0] ,
constraints=[ x^2+y^2+z^2<=1 ],
rhoend=1e-100 );

とすれば

[ [x=0.57735027556638,y=0.57735026855187,z=0.57735026345063 ],
4.4408920985006262*10^-16,462,0 ]

と確認できます．