前提知識

• 一階述語論理(FOL)を知っておく
  • 英語を一階述語論理に変換する

限量子記号消去(QE)アルゴリズムとその計算の現状

限量子記号消去アルゴリズムとその計算の現状について 佐藤洋祐

まとめ

• 実数領域における最初のQEアルゴリズムはTaiskiによって与えられたが、計算量を考慮していないため実際にプログラムとして実装しても使い物にならない。
• CADと呼ばれるQEアルゴリズムがMathmaticaなどで使われる実用的なアルゴリズムになる
• CGS-QEと呼ばれる高速のアルゴリズムが存在し、多数の等式を含む一階述語論理式に対する計算に有効
  • Real Quanti er Elimination by Computation ofComprehensive Grobner Systems

CADを実際に手元で使ってみる

• CAD(=Cylindrical Algebraic Decomposition)はCollinsによって1975年に発表された
  • Quantifier elimination for real closed fields by cylindrical algebraic decompostion
  • これも読む時間があったら読みたい

QEの教育用の実装が以下にあった

• QEPCAD
  • インストール方法等は以下を参照、Qiitaではないのでここには書かない
    • QEPCADのインストールと簡単な使い方
    • QEPCAD Version B 1.72

簡単な数式の解を求める

• qepcadに対してechoで数式を渡して解かせる例に従った

数学IAの参考書から

• $x^2+x-42=0$ の解は？

$ echo -e "[] \n (x) \n 1 \n [x^2+x-42=0]. \n finish" | qepcad
...略...
An equivalent quantifier-free formula:

x + 7 >= 0 /\ x - 6 <= 0 /\ [ x - 6 = 0 \/ x + 7 = 0 ]

おー、解けている

限量記号がついたFOLを渡して解かせる

ここからが本命で、$\forall$ と $\exists$ が入った式を解けないと意味がない

• $x^2+y^2=1$ の$y$の範囲は？

$ echo -e "[] \n (x,y) \n 1 \n (Ey)[x^2+y^2=1]. \n finish" | qepcad
...略...
An equivalent quantifier-free formula:

x + 1 >= 0 /\ x - 1 <= 0