情報実習II

数理論理学
第12回
導出原理１(準備)
© 加藤，高田，新出
4.2.1項(p. 89)
導出原理の概要
4.2.2項(p. 92)
単一化
課題11(教科書 p. 205 [6])
• quick_sort を参考に、大きいもの順に
数字のリストを並べ替えるプログラム、
quick_reverseを定義せよ。
?- quick_reverse([3, 8, 0, 5, 2, 1], List2).
List2 = [8, 5, 3, 2, 1, 0]
?- quick_reverse([ ], List2).
List2 = [ ]
課題11
?- quick_reverse([3, 8, 0, 5, 2, 1], List2).
List2 = [8, 5, 3, 2, 1, 0]
quick_reverse([Head | Tail], List2)
:- partition(Tail, Head, Small, Large),
quick_reverse(Small, ListS ),
quick_reverse(Large, ListL),
append( ListL, [Head | ListS], List2).
quick_reverse([], []).
4.2 導出原理による推論
(p. 89)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
4.2 導出原理による推論
(p. 89)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
4.2 導出原理による推論
(p. 89)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
冠頭連言標準形へ変換
yx( ( A( x)  B  )
 ( E  F  )

 ( P  Q  ) )
スコーレム標準形へ変換
y ( ( A( f ( y ))  B  )
C1
 ( E  F  )

C2
 ( P  Q  )Cm)
y( C1  C2  Cm )
4.1.4 節集合
p. 87
Fsk  x1x2 (C1  C2   Cm )
とする。このとき、
prologプログラム
に対応
S  {C1, C2 ,, Cm}
をFsk に対応する節集合という。また、
Fsk を S に対応するスコーレム標準形という。
定義 4.5 S の解釈は、 Fsk の解釈と同じ。
I(S) = I(Fsk)
4.2.1 導出原理の概要 (p. 89)
female(sumire).
parent(sumire,maruko).
mother(X,Y) :- parent(X,Y), female(X).
?- mother(sumire,maruko).
S={female(sumire),
parent(sumire,maruko),
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko)}
4.2.1 導出原理の概要 (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
4.2.1 導出原理の概要 (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
4.2.1 導出原理の概要 (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
4.2.1 導出原理の概要 (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
4.2.1 導出原理の概要 (p. 90)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
{sumire/x, maruko/y}
mother(sumire,maruko)∨￢parent(sumire,maruko)
∨￢female(sumire)
￢
mother(sumire,maruko)
￢parent(sumire,maruko)∨￢female(sumire)
節4.3 と 4.4 の導出節 (p. 90 ll. 4)
4.2.1 導出原理の概要 (p. 91)
{ female(sumire),
(4.1)
parent(sumire,maruko),
(4.2)
mother(x,y)∨￢parent(x,y)∨￢female(x),
￢ mother(sumire,maruko) }
(4.4)
(4.3)
￢parent(sumire,maruko)∨￢female(sumire)
￢female(sumire)
三段論法
p. 92, p. 41
(空節) mgu {sumire/x, maruko/y}
4.2 導出原理による推論
(p. 92)
4.2.1 導出原理の概要
4.2.2 単一化とmgu
• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu
4.2.3 導出原理を用いた推論手順
4.2.2 単一化と mgu (p. 92)
定義 3.16 代入 (p. 59)
θ ：シータ、 σ：シグマ
例 θ ={sumire/x, maruko/y}
定義 4.6 単一化、単一化代入
{L1, L2,..., Ln } : 項または論理式の集合
L1θ=L2θ=,..., =Lnθ となるとき
θは {L1, L2,..., Ln } の単一化代入
例 θ ={sumire/x, maruko/y} は
{mother(x,y), mother(sumire,maruko)}
の単一化代入
4.2.2 単一化と mgu (p. 93)
定義 4.7 不一致集合
{L1, L2,..., Ln } =S: 同じ述語記号を持つ
原子論理式の集合
各 Li を左から辿って最初に見つかる
一致しない項の集合が S の不一致集合
例4.9
L1 = mother(x,y),
L2 = mother(w,maruko)
{L1, L2} の不一致集合は {x,w}
4.2.2 単一化と mgu (p. 93)
定義 4.8 代入の合成 σ○θ
任意の項または論理式 F に対して
(F θ2)σ= F θ1 : θ1はθ2とσの合成
σ
θ
2
例 4.10
○
θ1 ={sumire/x, maruko/y, sumire/w}
θ2 ={w/x, maruko/y},
σ ={sumire/w}
mother(x,y) θ1 =mother(sumire,maruko)
mother(x,y) θ2 =mother(w,maruko)
mother(w,maruko)σ =mother(sumire,maruko)
4.2.2 単一化と mgu (pp. 94, 95)
定義 4.9 単一化アルゴリズム
例 4.11 S={mother(x,y) , mother(w,maruko)}
・ S0 ={mother(x,y) , mother(w,maruko)}
θ0=ε ={}
・ D0 ={x,w} x0=x, t0=w
S の単一化代入
・ θ1=θ0 ○{w/x}= {w/x}
S1 =S0θ1 ={mother(w,y), mother(w,maruko)}
・ D1 ={y,maruko} x1=y, t1=maruko
・ θ2=θ1 ○{maruko/y}= {w/x, maruko/y}
S2 =S1θ2 ={mother(w,maruko), mother(w,maruko)}
={mother(w,maruko)}
(p. 1 参照)
課題12 下記の S を単一化せよ
全て記述
S ={parent(hiroshi,y) , parent(v,z)} すること
・ S0 ={parent(hiroshi,y) , parent(v,z)}
θ0=ε ={}
・ D0 ={
・ θ1=θ0 ○{
S1 =S0θ1 ={
・ D1 ={
・ θ2=θ1 ○{
S2 =S1θ2 ={
} x0= ,
} ={
t0=
}
}
} x1= , t1=
}= {
={parent(hiroshi,z)}
}
}

Download Report