BOTTEMA2009

いわゆる「不等式の証明」がQEの代表的な応用であることは既にお話した通りですが，そこには
【１】パラメトリックシステム向けの汎用ツールでは効率が悪い
【２】過程が普通の証明の参考にならない
といった不満もあります．

というわけで今回は，何かと重くなったMaple上のツールでありながら，定係数またはワンパラの不等式に限定することで高速処理を実現している「BOTTEMA2009」をご紹介します．

まずは，コードファイルをダウンロード．
http://www.irgoc.org/download/file.php?id=7&sid=f73049cfa7535cd4b5504a54302c1982
カレントディレクトリに展開したら，Mapleを起動して

read "bottema2009";

とすれば準備完了です．

このBOTTEMA2009の特徴は

■多項式関数のみではなく，代数関数で表された不等式まで扱える

■弱い不等式，つまり，≧，≦で表された式しか扱えず，＞，＜を用いても正しい結果は一般には得られない

および

■処理が高速

と言う点でしょう．実装されている主な関数は，proverでは
prove(eq,[eq(s)])
sprove(eq)
xprove(eq,[eq(s)])
yprove(eq,[eq(s)])
最適化系では
cmin(eq,[eq(s)],var)
cmax(eq,[eq(s)],var)
xmin(eq,[eq(s)],var)
xmax(eq,[eq(s)],var)
です．

*proveの引数のineqは帰結の不等式，[ineq(s)]は仮定の不等式のリストで省略可です．

出力には「成立」「逆向きに成立」「有理数の反例を示して不成立」のパターンがあります．

proveは，ツールのメイン関数であり，その名からも判るようにBOTTEMA2009は，ユークリッド幾何の三角形に関する不等式の証明を念頭においたものなので，このproveでは，以下のように設定されています．

a, b, c, lengths of sides of the triangle
s, s:=(a+b+c)/2, half the perimeter
x, y, z, x:=s-a, y:=s-b, z:=s-c,
R, circumradius
r, radius of the incircle
ra, rb, rc, radii of excircles, respectively
ha, hb, hc, altitudes respectively
ma, mb, mc, lengths of medians, respectively
wa, wb, wc, bisectors of angles, respectively
S, Area of the triangle
d, distance from circumcenter to incenter
p, p:=4*r*(R-2*r)
q, q:=s^2-16*R*r+5*r^2
A, B, C, angles of the triangle, respectively
sin(A), sines of the angles, respectively
other trigonometric functions denoted analogously

一方，xproveでは仮定・帰結に現れる各変数が非負値と設定されているだけで，対称な多項式用のsproveも同じ設定です．ただし，sproveはDifference Substitutionというアルゴリズムを採用し一般に高速ですが，仮定が付いたり，次数・変数の個数によっては他の*proveを呼びます．

yproveは汎用です．

続く，*min,*maxは，仮定[ineq(s)]のもとで，つねに帰結のineqが成り立つような，varの最小値，最大値を出力するもので
cmin,cmaxはproveと同じく３角形用
ccmin,ccmaxは最適解が２等辺３角形であることを前提とし
findmin,findmaxは内部でc,ccに振り分けて実行する（旧バージョンである「BOTTEST9」では３辺の長さに関して対称な多項式用）
xmin,xmaxはxproveと同じく非負値変数用
です．なお，*proveと違い，仮定が空のときも空の仮定[ ]を書かないと叱られます．

また，最適化系の関数は他にも，varの範囲・ステップを指定して近似値を得るfmin(ineq,strat,end,dig,[ineq(s)]),fmax,xfmin,xfmaxなども実装されています．