simplest CAD

　前回は解集合の図のみを正射影で求めるグラフィカルな QE でしたが，関数の種類，変数の個数が手頃であれば，同様の方法により，シンボリックに QE できます．
　例えば

(1)　∃x ( a≦x≦a+2 ∧ x^2-2 x+a≦0 )

を考えましょう．人間なら a について場合を分ける所ですが，ある種の連立方程式さえ解ければ，文字通り機械的に QE できます．
　すなわち，a が (1) を満たすとは，xy 平面において，直線 y=a が

y≦x≦y+2 ∧ x^2-2 x+y≦0

つまり

x-2≦y≦x ∧ y≦-x^2+2 x

の表す図形と点を共有することなので，2 直線 y=x-2,y=x と放物線 y=-x^2+2 x の共有点の y 座標さえ求めれば，(1) と等価な式

-3≦a≦1

が得られます．
　次に，全称量化を QE してみます．前回は，否定をとって特称量化に帰着しましたが，今回は直接扱います（ここがポイントです）．すなわち，a が

∀x P(x,a)

を満たすとは，xy 平面において，直線 y=a 上の任意の点が図形 P(x,y) に属する，つまり，直線 y=a が図形 P(x,y) に含まれることなので，例えば

(2)　∀x ( a≦x≦a+2 → x^2-2 x+a＞0 )

を QE するなら

y≦x≦y+2 → x^2-2 x+y＞0

つまり

( x＜y ∨ y＜x-2 ) ∨ y＞-x^2+2 x

の表す図形に直線 y=a が含まれるという式

a＜-3 ∨ 1＜a

がその結果です．
　今回述べた方法は，1975年に Colins 博士が発表した CAD (Cylindrical Algebraic Decomposition) Metapress | A Fast Growing Resource for Young Entrepreneurs を用いた QE の極端に簡単な，すなわち，束縛変数，自由変数の個数がともに 1 の場合にあたり，上記の特称，全称の真偽判定方法は，空間を有限個に分割して，無限を有限に帰する CAD による QE の重要なコンセプトです．
　CAD は，発表から約35年，その実装が可能となってから約20年を経た現在においてなお，最も一般的な QE アルゴリズムであり，このブログでも順次お話して行く予定です．