数理論理学

第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([Head | Tail], List2)

:- partition(Tail, Head, Small, Large),

quick_reverse(Small, ListS ),

quick_reverse(Large, ListL),

append( ListL, [Head | ListS], List2).

quick_reverse([], []).

?- quick_reverse([3, 8, 0, 5, 2, 1], List2).

List2 = [8, 5, 3, 2, 1, 0]

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 導出原理を用いた推論手順

冠頭連言標準形へ変換

スコーレム標準形へ変換

C1

C2

Cm

4.1.4 節集合

とする。このとき、

​

​

をFsk に対応する節集合という。また、

Fsk を S に対応するスコーレム標準形という。　

prologプログラム

に対応

定義 4.5 S の解釈は、 Fsk の解釈と同じ。

　　　 I(S) = I(Fsk)

p. 87

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)}

{ female(sumire), (4.1)

parent(sumire,maruko), (4.2)

mother(x,y)∨￢parent(x,y)∨￢female(x), (4.3)

￢ mother(sumire,maruko) } (4.4)

4.2.1 導出原理の概要 (p. 90)

{ female(sumire), (4.1)

parent(sumire,maruko), (4.2)

mother(x,y)∨￢parent(x,y)∨￢female(x), (4.3)

￢ mother(sumire,maruko) } (4.4)

4.2.1 導出原理の概要 (p. 90)

{ female(sumire), (4.1)

parent(sumire,maruko), (4.2)

mother(x,y)∨￢parent(x,y)∨￢female(x), (4.3)

￢ mother(sumire,maruko) } (4.4)

{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), (4.3)

￢ mother(sumire,maruko) } (4.4)

{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), (4.3)

￢ mother(sumire,maruko) } (4.4)

{sumire/x, maruko/y}

mother(sumire,maruko)∨￢parent(sumire,maruko) ∨￢female(sumire)

￢ mother(sumire,maruko)

4.2.1 導出原理の概要 (p. 90)

￢parent(sumire,maruko)∨￢female(sumire)

節4.3 と 4.4 の導出節 (p. 90 ll. 4)

￢parent(sumire,maruko)∨￢female(sumire)

parent(sumire,maruko)

￢female(sumire)

female(sumire)

(空節)

4.2.1 導出原理の概要 (p. 91)

{ female(sumire), (4.1)

parent(sumire,maruko), (4.2)

mother(x,y)∨￢parent(x,y)∨￢female(x), (4.3)

￢ mother(sumire,maruko) } (4.4)

mgu {sumire/x, maruko/y}

三段論法

p. 92, p. 41

4.2 導出原理による推論 (p. 92)

4.2.1 導出原理の概要

　 4.2.2 単一化とmgu

• 単一化代入
• 不一致集合
• 代入の合成
• 単一化アルゴリズム
• mgu

4.2.3 導出原理を用いた推論手順

定義 3.16 代入 (p. 59)

　θ ：シータ、 σ：シグマ　

例　θ ={sumire/x, maruko/y}

4.2.2 単一化と mgu (p. 92)

定義 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.8 代入の合成 　 σ○θ

任意の項または論理式 F に対して

(F θ2)σ= F θ1

4.2.2 単一化と mgu (p. 93)

例 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)

: θ1はθ2とσの合成

σ ○ θ2

定義 4.9 単一化アルゴリズム

4.2.2 単一化と mgu (pp. 94, 95)

例 4.11 S={mother(x,y) , mother(w,maruko)}

・　S0 ={mother(x,y) , mother(w,maruko)}

・　D0 ={x,w}

x0=x, t0=w

θ0=ε ={}

・　θ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)}

・　D0 ={　　　　　}

x0= , t0=

θ0=ε ={}

・　D1 ={ }

x1= , t1=

S2 =S1θ2 ={ }

={parent(hiroshi,z)}　

S1 =S0θ1 ={ }

・　θ2=θ1 ○{ }= { }

・　θ1=θ0 ○{ } ={ }

全て記述

すること