Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

-数学- 量限定子除去 : ちょっと変わった数式処理

 

f:id:jurupapa:20140402102124j:plain

にほんブログ村 科学ブログ 数学へ
にほんブログ村

 

数式処理の専門家の人はよく知っているのが、そうでない人は全く知らない、そんな技術の一つが量限定子除去と呼ばれる技術です。英語ではQuantifier Elimination, 略してQ.E.とも言われます。

 

具体的には実数の世界に限定して、多項式を項とする、等号や不等号を述語とする1階述語論理の世界を考えます。例えば、

$$ x^2\geq 0$$

は不等号を述語とし、多項式を項とする式です。これに全称量限定子を付けてみます。

$$ \forall x,\, x^2\geq 0$$

この式は確かに成り立ちます。

$$ \mathbf{true}$$

となります。Q.E.の用語で言えば、(2)に量限定子除去を適用すると(3)が得られる、という訳です。

別の例題を考えてみます。

f:id:jurupapa:20140422001257p:plain

これは \( y=x^3-6\,x \) という関数のグラフです。このグラフを見ると大体ですが、\( -\frac{5}{2}\leq x \)の範囲では \( y > -6 \) が成り立ちそうです。論理式で書いてみると、

$$\forall x\, \left(x\geq -\frac{5}{2}\right) \implies \left(x^3-6\,x>-6\right)$$

この(4)もQ.E.を適用すると\( \mathbf{true} \)が得られるはずです。でも\( x>-3 \) の範囲では成り立ちそうにありません。つまり、

$$\forall x\, \left(x\geq -3 \right) \implies \left(x^3-6\,x>-6\right)$$

にQ.E.を適用すると \( \mathbf{false} \) が得られるでしょう。

このように真偽値が決まる文に対してQ.E.を適用すると、その文の真偽を決定することになります。

This is a test.
天気