FreeStyleWiki

限量記号消去法(QE)

このエントリーをはてなブックマークに追加

[数学]

限量記号消去法(QE)

\begin{align*} & 限量子記号消去(Quantfier Elimination、以下ではQEと略記する)とは \\ & 代数的な一階述語論理式から限量子記号 \forall と \exists を取り除き、それと等価な自由変数のみの代数的な式を求めることである。 \end{align*}

まとめ

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

TaiskiとCADのアルゴリズムに関してはMITの公開講座に解説があったので、読んでいく

  QEアルゴリズム(Taiski)

  QEアルゴリズム(CAD=Cylindrical Algebraic Decomposition)

  QEアルゴリズム(CGS-QE)