Fourier–Motzkin消去法
以下の手順を繰り返し行い、限量子を除去していく。変数の定義域は実数もしくは有理数。
以下の置き換えを行う。 等式や不等式に ¬ がかかる物は反転させる。 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 の変換を行う。
下記公式を使い、限量子を除去する。 ∃ x .