Hatena::Groupxn--272ax3f

論理と計算のしくみ4.4

論理と計算のしくみ4.4

プレゼンテーション

プレスバーガ算術

4.3(c) の通り 算術における閉じた論理式が真か偽かは決定不能.

算術の言語を制限すると決定可能になる場合がある.

アウトライン

  • 決定可能なプレスバーガ算術の構文論と意味論
  • 真か偽か決定するクーパのアルゴリズム

プレスバーガ算術の構文論/意味論

掛け算がない.

  • 定数記号  0, 1
  • 関数記号  +, -
  • 述語記号  <

整数定数倍は可能

  •  3x := x + x+ x
  •  xy is undefined
  •  x=y:= x<y+1 \wedge y<x+1
  •  c|e:= c  e を割り切る (c は定数)
  • 例: ( 3|x:= \exists y (x = y + y + y))

簡単のため標準構造の領域は整数全体.

クーパのアルゴリズム

プレスバーガ算術の任意の閉じた論理式はその標準構造において真であるか決定可能

限定子を取り除くことができる.

  1.  \forall , = の除去 (  \forall x A\[x\] =>  \neg\exists x \neg A\[x\]
  2.  \exists x A\[x\] を内側から \exists を取り除く
    1. #  A\[x\]\exists\forall も含まない
    2.  \neg の移動  c|t の前にしか現れないように
    3. 定数項の除去  \exists x A\[x\] => \exists x A'\[cx\] => \exists xA'\[x\] \wedge c|x (c>0)
    4. # 論理式は x<t, x>t, d|x+t の形のみからならる. ( tx を含まない )
    5. \exists を含まない形に変形

定数項の除去

x が比較の片側にしか現れないように移項

x の係数の最小公倍数になるように 定数倍

例えば

 4x < x + y \vee \neg 3|2x+z

=>  3x < y \vee \neg 3|2x+z

=>  6x < 2y \vee \neg 9|6x+3z

限定子の除去

  •  A'\[x\]x の係数は 全て1
  • 論理式は x<t, x>t, d|x+t の形のみからならる. ( tx を含まない )
  • \negd|x+t の前にしか現れない

 \exists x A\[x\] が真になる場合を二つに

  1. (1)  A\[x\] を真にする最小のxが存在しない
  2. (2)  A\[x\] を真にする最小のxが存在する

(1) の場合

  •  A\[x\] を満たすいくらでも小さいx が存在
  •  x<t を 真,  t>x を 偽 に置き換えた式を =>  A_{-\infty}\[x\]
  •  d|x+t という形の論理式しか現れない
  •  d_1 \dots d_n の最小公倍数 \delta とすると  A_{-\infty}\[j\] (j = 1 \dots \delta ) を調べる.

(2) の場合

  • どれかの  t<x をぎりぎりで成り立たせている. (  t<x  \neg の中にない)
  •  D := \{ t \mid t<x  A\[x\] 原子論理式 }
  •  A\[t+j\] (t\in D, j = 1, \dots, \delta  ) を調べる.

全部選言とる.

 \bigvee_{j=1,\dots, \delta} A_{-\infty}\[j\] \vee \bigvee_{j=1, \dots, \delta} \bigvee_{t \in D} A\[t+j\] 決定可能