Homeにもどる

Mathematica による QE 計算の基本

ここでは、数式処理システム Mathematica による QE 計算に必要な事項について説明します。

Mathematica での数式一般の扱い方については Mathematica による計算の基本 を参照してください。

Mathematica の論理演算

• 連言（かつ）: $f_1 \land \cdots \land f_n$
  • f1 && … && fn
  • And[f1,…,fn]
• 選言（または）: $f_1 \lor \cdots \lor f_n$
  • f1 || … || fn
  • Or[f1,…,fn]
• 否定（…でない）: $\lnot f$
  • ! f
  • Not[f]
• 含意（ならば）: $f \Rightarrow g$
  • f [Esc] => [Esc] g
    • Escapeキーを押してから => と書き、さらにEscapeキーを押してから右辺を書きます。
  • Implies[f, g]
• 同値: $f \Leftrightarrow g$
  • Equivalent[f, g]

Mathematica における量化子（限量子, 限量記号）

• 存在量化子（存在して）: $\exists x (f)$ – ある $x$ が存在して $f$ が成り立つ
  • Exists[x, f]
• 全称量化子（すべての）: $\forall x (f)$ – すべての $x$ に対して $f$ が成り立つ
  • ForAll[x, f]
• 量化子がついた変数を「束縛変数」と呼びます。
• 量化子がついていない変数を「自由変数」と呼びます。

Mathematica における量化子消去 (QE)

• Reduce[L, Reals]
  • L: 論理式
  • Reals: 実数の範囲内で問題を解くためのオプション