情報実習II

数理論理学
第10回
論理式の標準形
© 加藤，高田，新出
4.1節(p. 77)
論理式の標準形
演習課題 9 定理3.1の証明
E と F が論理的に等価 (E ≡ F) である
iff ( if and only if)
任意の解釈 I に対して I(E) = I(F)
を証明せよ
(1) ⇒ の証明：
E と F が等価であること (E ≡ F) を仮定する。
定義3.20より、F は E の論理的帰結である。よって、
定義3.19より I(E)=Tとなる任意の解釈 I に対して、
I (F)=Tである。
さらに E は F の論理的帰結なので、 I (F)= T
となる任意の解釈 I に対して、I(E)=Tである。
以上より、任意の解釈 I に対して、 I(E)= I(F)となる。
⇒
(2)
の証明：
任意の解釈 I に対して、 I(E)= I(F)
を仮定する。このとき I(E)= T
(a)
(b)
となる任意の解釈 I に対して、I (F)= T
(c)
である。従って、定義3.19より
F はE の論理的帰結
(d)
となり、かつ、同様に E も F の論理的帰結
となる。よって定義3.20
より、E と F は論理的に等価
(d)
(e)
である。
(f)
⇒
(2)
の証明：
任意の解釈 I に対して、 I(E)= I(F)
を仮定する。このとき I(E)= T
(a)
(b)
となる任意の解釈 I に対して、I (F)= T
(c)
である。従って、定義3.19より
F はE の論理的帰結
(d)
となり、かつ、同様に E も F の論理的帰結
となる。よって定義3.20
(d)
(e)
より、E と F は論理的に等価
である。
(f)
定理3.1
閉論理式 E と F に対して、
E ≡ F iff 任意の解釈 I に対して I(E)=I(F)
I
I
I1
I
E のすべてのモデル
I2
Im
F のモデルでもある。
I
I
I
prologプログラム
：
の動作原理である
：
parent(sumire, maruko).導出演繹の準備
：
female(sumire).
：
mother(X,Y) :- parent(X,Y), female(X).
?- mother(sumire, maruko).
true
解釈 I を I ( D ,A ) とする。ただし
D  {tomozou, kotake, hiroshi, sumire, sakiko, maruko}
A(parent)(sumire, maruko)=T
：
A(female)(sumire)=T この解釈の元で、
：
∀X,Y (parent(X,Y) ∧ female(X)
⊃ (mother(X,Y))
∧mother(sumire, maruko).
この式が T (真)となるか
人間の知的作業による証明 (p. 64)
計算機では
ちょっと無理
∀X,Y (parent(X,Y) ∧ female(X)
⊃ (mother(X,Y))
導出計算機などで自動的に上のような
原理式の真偽をチェックするためには、
変換任意の論理式を標準形(節集合)
に変換する必要がある。
mother(X,Y) ∨ ￢parent(X,Y)∨￢ female(X)
∀X,Y (parent(X,Y) ∧ female(X)
⊃ (mother(X,Y))
導出計算機などで自動的に上のような
原理式の真偽をチェックするためには、
変換任意の論理式を標準形(節集合)
に変換する必要がある。
mother(X,Y) :- parent(X,Y), female(X).
E= ∀X,Y (parent(X,Y) ∧ female(X)
⊃ (mother(X,Y))
:
:
F= mother(X,Y) :- parent(X,Y), female(X).
前回
論理式 E を論理式F に変換するとき、どの
ような条件が満たされれば変換してよいか?
定理 3.1
今日
論理式 E を論理式 F へ変換する手順
定理の自動証明(導出原理)
のための準備（その２）
x( hum an( x)  m ortal( x))
 hum an(a)
 mortal(a)
導出原理: 論理式が恒偽かどうかを組織的に証明
するための方法。
論理式を導出原理にかけるためには、標準形に
変形する必要がある。
重要な等価論理式
(p. 74-75 1～24式)
10. E  F  E  F :
証明はp.68 例3.10
8. ( E  F )  E  F
9. ( E  F )  E  F
11. (x ( E ))  x (E )
12. (x ( E ))  x (E )
1～24の規則を使って、任意の論理式を
導出原理で扱える節形式へと変換できる
F = "x( human(x)É mortal (x))
Ù human(a) É mortal(a)
冠頭標準形 (p. 78 定義4.1)
$x( human(x)ÙØmortal (x)
ÚØhuman(a)Úmortal(a) )
冠頭連言標準形(p. 80 定義4.2)
$x((human(x)ÚØhuman(c)Úmortal(c))
Ù(Ømortal (x)ÚØhuman(c)Úmortal(c)))
スコーレム標準形(p. 82 定義4.3)
(human(a)ÚØhuman(c)Úmortal(c))
Ù(Ømortal (a)ÚØhuman(c)Úmortal(c))
スコーレム標準形(∃除去)
(p. 82 定義4.3)
(p. 84 例4.4)
Fpc  xyz (( p ( x, z )  q ( y, z ))  r ( x, y ))
「ある x」「ある y」を適当な定数で置き換える
Fsk  z (( p (a, z )  q (b, z ))  r (a, b))
スコーレム定数(p. 83 ステップ5)
スコーレム標準形(∃除去)
(p. 82 定義4.3)
(p. 84-85 例4.5)
Fpc1  zxy (( p ( x, z )  q ( y, z ))  r ( x, y ))
「ある x」「ある y」は z の影響を受けているので
適当な関数記号 f と g を用いて
Fsk1  z (( p ( f ( z ), z )  q ( g ( z ), z ))  r ( f ( z ), g ( z )))
スコーレム関数記号(p. 83 ステップ5)
スコーレム標準形(∃除去)
(p. 85)
Fpc1  x parent ( x, maruko)
「ある x」を適当な定数で置き換え
Fsk1  parent (hiroshi, maruko)
スコーレム標準形(∃除去)
(p. 86)
Fpc 2  yx parent ( x, y )
「ある x」は y の影響を受けている
Fsk 2  y parent (itsParent ( y ), y )
y parent (hiroshi, y )
スコーレム標準形(∃除去)
(p. 82 定義4.3)
(p. 85 例4.6)
Fpc 2  wxzy (( p ( x, z )  q ( y, z ))
 (r ( w, y )  s ( w, x)))
「ある x」は w の、「ある y」は wとzの影響を
受けているので適当な関数記号 f と g を用いて
Fsk 2 
wz (( p ( f ( w), z )  q ( g ( w, z ), z ))
 (r ( w, g ( w, z ))  s ( w, f ( w))))
F  x( human ( x)  mortal ( x))
 human(a )  mortal (a )
冠頭標準形 (p. 78 定義4.1)
$x( human(x)ÙØmortal (x)
ÚØhuman(a)Úmortal(a) )
冠頭連言標準形(p. 80 定義4.2)
x( (hum an( x)  hum an(a)  m ortal(a) )
 ( m ortal( x)  hum an(a)  m ortal(a) ))
スコーレム標準形(p. 82 定義4.3)
(hum an(a)  hum an(a)  m ortal(a) )
 ( m ortal(a)  hum an(a)  m ortal(a) )
冠頭標準形へ変換中(p. 79 例 4.1)
F  x( human ( x)  mortal ( x))
E
1
 human(c)  mortal (c)
⊃ 除去（p. 74
E2
10.)
E1  E2  E1  E2
 (x( human ( x)  mortal ( x))
 human(c))  mortal (c) E1
E2
冠頭標準形へ変換中(p. 79 例 4.1)
F  (x( human ( x)  mortal ( x))
 human(c))  mortal (c)
⊃ 除去（p. 74
10.)
 (x( human ( x)  mortal ( x))
 human(c))  mortal (c)
冠頭標準形へ変換中(p. 79 例 4.1)
(x( human ( x)  mortal ( x))
E11
 human(c))  mortal (c)
E12
￢移動（ド・モルガンの法則 p. 74
8.)
( E11  E12 )  E11  E12
 x( human ( x)  mortal ( x))
E'11
 human(c)  mortal (c)
冠頭標準形へ変換中(p. 79 例 4.1)
x( human ( x)  mortal ( x))
E'
11
 human(c)  mortal (c)
￢移動（p. 74 11.)
(x ( E ))  x (E )
 x( human ( x)  mortal ( x))
 human(c)  mortal (c) E''11
冠頭標準形へ変換中(p. 79 例 4.1)
$xØ(Øhuman(x)Úmortal (x))
ÚØhuman(c)Úmortal(c)
￢移動（ド・モルガンの法則 p. 74
9.)
( E  F )  E  F
 x(( hum an( x))  m ortal( x))
 hum an(a)  m ortal(a)
冠頭標準形へ変換完了
x(( human ( x))  mortal ( x))
 human(c)  mortal (c)
二重否定則（p. 74
5.) とスコープ拡張
 x(human ( x)  mortal ( x)
 human(c)  mortal (c))
 Fp
冠頭連言標準形へ変換
yx( A  B  )
 ( E  F  )

 ( P  Q  )
冠頭連言標準形へ変換(p. 82 例 4.2)
Fp  x( human ( x)   mortal ( x)
E2
E1
 human(c)  mortal (c) )
∨分配
(p. 74 7. )
E3
E3  ( E1  E2 )  ( E3  E1 )  ( E3  E2 )
 x(
(human ( x)  human(c)  mortal (c) ) E3
E1
 ( mortal ( x)  human(c)  mortal (c) )
E2
E3
)  Fpc
スコーレム標準形(∃除去)
Fpc1  x parent ( x, maruko)
「ある x」を適当な定数で置き換え
Fsk1  parent (hiroshi, maruko)
スコーレム標準形へ変換
冠頭標準形連言標準形
x( (human ( x)  human(c)  mortal (c) )
 ( mortal ( x)  human(c)  mortal (c) ))
x に定数 a を代入
スコーレム標準形
(human (a )  human(c)  motal (c) )
 ( motal (a )  human(c)  motal (c) )
演習課題 10
xv(r ( x, v))  zw(q( z, w))
をスコーレム標準形に変換せよ。
スコーレム関数記号は、x に影響を受けるもの
はf (x)を、x と z に影響を受けるものはg(x,z)
を使用すること。
途中の経過式、および使った規則も全て記入すること。
これらが一つでも欠けていれば０点。
以下のヒントも含め、全て記述すること
xv(r ( x, v))  zw(q( z, w))
⊃ 除去(p. 74 10.)
 (xv(r ( x, v)))  zw(q( z, w
(a)))
￢移動 (p. 74 12,11)
 xv(b)
(r ( x, v))  zw(q( z,(a)
w))
∀,∃移動
 xvzw(r ( x, v)  q( z,(c)
w))
∃削除(スコーレム化)
 xz(r ( x, f ( x))  q( z, g ( x, z(d)
)))

Download Report