Fourier–Motzkin消去法

Fourier–Motzkin消去法（）とは、数理論理学および計算機科学において、一次不等式からなる一階述語論理式の限量子（∀や∃）を除去するアルゴリズム。限量子消去法（）の1つ。1826年にジョゼフ・フーリエが発見し、1918年に L. L. Dines が再発見し、1936年に Theodore Motzkin が再々発見した。
アルゴリズム.
以下の手順を繰り返し行い、限量子を除去していく。変数の定義域は実数もしくは有理数。
具体例.
formula_7 に対して、Fourier–Motzkin消去法を使用し、簡略化する。
 formula_7
 formula_9
 formula_10
 formula_11
 formula_12
 formula_13
 formula_14
 formula_15
 ここで公式を使用する。
 formula_16
 formula_17
 formula_18
 formula_19
 formula_20
整数への拡張.
変数の定義域を整数にする場合の拡張を William Pugh が1992年に発表している。オメガテストと名付けた判定条件を追加している。
また、1972年に D. C. Cooper がFourier–Motzkin消去法の直接の拡張ではないが、整数変数に対する限量子消去法であるCooper法を発表している。
多項式の場合.
一次式ではなく、より一般的な多項式の場合 George E. Collins が1975年に発表した Cylindrical Algebraic Decomposition (CAD) を使用することにより、限量子消去が出来る。