使い方その１

QEPCAD Bには複数の入力方法があります．今回は（やや大変ですが）対話モードの使い方をお話しましょう．例として，xy平面上の曲線x^2+y^2=1と直線ax+by=1とに共有点が存在するという条件を処理します．

　まず前回のように端末より

qepcad

と入力，エンターキーを押すと，QEPCAD Bの起動画面に続いて

Enter an informal description between '[' and ']':

と表示されますので，コメントは空のまま

[]

と入力，エンターキーを押すと

Enter a variable list:

のように処理する論理式に含まれる変数のリストを尋ねられますので

(a,b,x,y)

と入力します．ここでルールがあります．

ルール１）自由変数を先に，束縛変数を後に書き，束縛変数は論理式に現れる順に書く

下で示すように今回入力する論理式では(E x)(E y)の順に現れますので，(a,b,y,x)などと書くと後で叱られます．それではエンターキーを押してください．すると

Enter the number of free variables:

のように自由変数の個数を尋ねられますので

2

と入力，エンターキーを押すと

Enter a prenex formula:

と表示されます．ここにもルールがあります．

ルール２）入力する論理式はprenex formula（すべての量化子が先頭にある論理式）か，quantifier free formula（量化子を含まない論理式）に限る

任意の論理式は，このどちらかに変形できるのですが，量化子を多数含む式をprenexにするのは人間の業ではありませんので，このブログではRedLogのrlpnf関数を用います．今回の例は最初からprenexなので，そのまま

(E x)(E y)[x^2+x y+y^2-1=0 /\ a x+b y-1=0].

と入力します．書式は，まず

(量化子 束縛変数)

を列挙します．具体的には

(E x)

は「あるxについて」ということ，対して

(A x)

は「すべてのxについて」ということで，他にもQEPCAD Bには

(Xk x)

という「丁度k個の異なるxについて」なども実装されています．なお，量化子と束縛変数との間のスペースは略せます．それに続く部分は

[量化子を含まない論理式].

の書式で最後にピリオドが必要です．論理式は，多項式についての方程式，不等式（原子論理式）および

~ [論理式]
[論理式] /\ [論理式]
[論理式] \/ [論理式]
[論理式] ==> [論理式]
[論理式] <== [論理式]
[論理式] <==> [論理式]

の何れかであり，一番内側の[]は略せます．従って今回の例では

[x^2+y^2-1=0] /\ [a x+b y-1=0]

とするのが省略のない書き方です．また，結合の強弱は設定されていませんので[]が必要です．例えば

[x=1 /\ y=1] ==> x+y=2

を

x=1 /\ y=1 ==> x+y=2

と書くと叱られます．なお，方程式，不等式内での括弧は()，不等号は/=です．
　それではエンターキーを押してください．すると

Before Normalization >

と表示されますので，今回は最短コースなので，入力完了という意味で

finish

と入力，エンターキーを押すと，漸く結果が表示されます．
　お疲れ様でした．QEPCAD Bは自明な前処理を人間が行い，QEや簡約だけを実行するものなので入力はやや面倒です．しかし，QEPCAD Bはpartial CAD（partial cylindrical algebraic decomposition）というQEの原理の生みの親であるCollins博士の愛弟子Hoon Hong博士がその理論のインプリメンテーションとして1991年に製作した史上初のQEプログラムQEPCADの直系であり，後発の強みと強大な開発力をもつMathematica上のQEシステムに劣らぬ処理能力を有していることを踏まえれば，それだけの価値は充分にあると思います．
　次回は，まとめて入力でき，繰り返し利用できるバッチモードの使い方をお話します．