Homeにもどる

QEの計算例: 存在量化子 $\exists$ を含む論理式の量化子消去

例題

方程式 $x^2+bx+c=0$ が実根（実数解）をもつための $b, c$ の条件を求めよ。

解法

1階述語論理式の構成

この問題で示すべき条件を書き出すと

ある実数 $x$ が存在して $x^2+bx+c=0$ が成り立つ

となりますので、この問題を表す1階述語論理式は

$$\exists x (x^2 + b x + c = 0)$$

となります。

Mathematica への論理式の入力とQEによる解法

Mathematica に入力する論理式を定義します。

f1 = Exists[x, x^2 + b x + c == 0]

Reduce関数に論理式を入力して量化子消去を実行します。

Reduce[f1, Reals]

すると、次の出力が得られます。

c <= 0 || (c > 0 && (b <= -2 Sqrt[c] || b >= 2 Sqrt[c]))

出力の意味は次の論理式です:

$$c\le 0 \vee (c > 0 \wedge (b \le -2 \sqrt{c} \vee b \ge 2 \sqrt{c})))$$

ちょっと複雑ですね。

実は、Mathematica で QE を行う Reduce 関数は、変数を消去する順序を変えることができます。次のように実行してみましょう。

Reduce[f1, {b, c}, Reals]

すると、次の出力を得ます。

c <= b^2/4

この出力は、$x^2+bx+c$ の判別式から導かれる条件 $b^2-4c\ge 0$ に一致することがわかります。

ちなみに、最初のQE計算の出力は、変数を消去する順序を {c,b} に設定した結果であることがわかります。

Reduce[f1, {c, b}, Reals]
c <= 0 || (c > 0 && (b <= -2 Sqrt[c] || b >= 2 Sqrt[c]))

ここでは詳しい説明は省略しますが、Mathematicaが用いるQEアルゴリズムには、変数を消去する順序が存在し、その順序を変えることで、求まる論理式の形が変わることがあります。

ついでに、Mathematica で判別式は以下のように計算できます。

Discriminant[x^2 + b x + c, x]
b^2 - 4 c

Mathematica で判別式を求める時は、関数の主変数（ここでは $x$ ）を明記して入力します。