|
Fourier–Motzkin消去法（）とは、数理論理学および計算機科学において、一次不等式からなる一階述語論理式の限量子（∀や∃）を除去するアルゴリズム。限定記号消去法（）の1つ。1826年にジョゼフ・フーリエが発見し、1918年に L. L. Dines が再発見し、1936年に Theodore Motzkin が再々発見した〔Satisfiability Checking Fourier–Motzkin Variable Elimination 〕。 == アルゴリズム == 以下の手順を繰り返し行い、限量子を除去していく〔Arithmetic Decision Procedures: a simple introduction 〕。変数の定義域は実数もしくは有理数。 # 以下の置き換えを行う。 ## 等式や不等式に ￢ がかかる物は反転させる。 ## a ≧ b は b ≦ a へ ## a ＞ b は b ＜ a へ ## a ＝ b は (a ≦ b) ∧ (b ≦ a) へ ## ∀x. P(x) は ￢ ∃x. ￢ P(x) へ # 下記簡略化は随時行う。 ## 常に成り立つ もしくは 常に不成立な不等式は真や偽に置き換える。 ## 真や偽が ∧ や ∨ や ￢ に付く場合は適切に論理式を簡略化する。 ## ∃x. P(x) の形式において、P(x) が x を使用してなければ、∃x. を取り除く。 # ∃x. P(x) の形式で、P(x) に限量子が出てこない物を探し、P(x) を選言標準形に変換する。 # ∃x. (P(x) ∨ Q(x)) ⇔ (∃x. P(x)) ∨ (∃x. Q(x)) の変換を行う。 # Q が x を使用していない場合、∃x. (P(x) ∧ Q) ⇔ (∃x. P(x)) ∧ Q の変換を行う。 # 下記公式を使い、限量子を除去する。 #: #: :: 上記は一般的な形式だが、より分かりやすく、2つの不等式の場合に書き下すと以下の通り。 ::: ::: ::: ::: 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Fourier–Motzkin消去法」の詳細全文を読む スポンサード リンク
|