講義資料

人工知能特論2011
資料No.6
東京工科大学大学院
担当教員 亀田弘之
前回までの確認から
Prenex Conjunctive Normal Form
• Literal
• Clause
• PCNF
前回までこんな
話をしました。
3
Leteral
• Literalの定義:
1. アトムはリテラル (例: P(x), Q(3,5,8) )
2. アトムの否定もリテラル (例: ~P(x), ~Q(3,5,8))
– 上記の1を正リテラル(positive literal)、
2を負リテラル(negative literal) という。
(例: P(f(x)) は正リテラル, ~P(f(x)) は
負リテラル)
4
Clause
• Clauseの定義:
– ゼロ個以上かつ有限個のリテラルからなる選言
のこと。
例:
1. P(a) v Q(x,b,f(s))
2. ~Q(x,y) <=1個のリテラルの選言!
5
Clauseの集合による表記法
1. P(a) v Q(x,b,f(s))
 {P(a) , Q(x,b,f(s))}
2. ~Q(x,y)  {~Q(x,y) }
いろいろな表記法
があります。慣れる
しかありません。
6
Prenex Conjunctive Normal Form
q1 x1 qn xn (C1   Cm )
qiはかであり、 x1 , x2 ,, xnはすべて論理式に現れ る変数
7
Prenex Conjunctive Normal Form
Clause
q1 x1 qn xn (C1   Cm )
Prenex
Matrix
qiはかであり、 x1 , x2 ,, xnはすべて論理式に現れ る変数
8
PCNFの例
 xy (( P( x) ~ Q( x, y ))  (~ R(a, b) ~ P(a )))
 xyz ( S ( x, y, z )  P( y, z ))
 x(( P(a)  P(b))  ~ Q(a, x)  P( x)  (~ P(b)  Q( x, x)))
 x ~ y ( P( y )  Q( y, a ))
 x( P( x)  Q( x, a))
 ~ y (Q( y, a ))
9
PCNFへの変形
• 任意の述語論理式はPCNFに変形すること
ができる。その際、その論理式の真理値は保
存される。
• 例: xP( x)  xQ( x)
 ~ xP( x)  xQ( x)
 ~ xP( x)  yQ ( y )
 x ~ P ( x)  yQ ( y )
 x(~ P ( x)  yQ ( y ))
 xy (~ P ( x)  Q ( y ))
10
定理
• 任意の論理式φに対して、φと真理値が等価
な論理式ψでかつPCNFのものが1つ存在す
る。
11
変形の手順(その1)
1. 論理式φの中の→と↔を次の規則を用いて
取り除く。
1. (A→B) を (~A v B) に置き換える。
2. (A↔B) を (~A v B)^(A v ~B) に置き換える。
2. 分離された変数がそれぞれ異なるように変
数名を書き換える。
12
変形の手順(その2)
3. すべての~がアトムの直前に来るように次
の規則を用いて変形する。
1.
2.
3.
4.
5.
~∀x ψ を ∃x~ψ に置き換える。
~∃ x ψ を ∀x~ψ に置き換える。
~( φ ∨ ψ ) を ( ~φ ∧ ~ψ ) に置き換える。
~( φ ∧ ψ ) を ( ~φ ∨ ~ψ ) に置き換える。
~~φ を φ に置き換える。
13
変形の手順(その3)
4. すべての限量子∀と∃を論理式の先頭部分
へ移動させる。
1.
2.
3.
4.
5.
6.
7.
8.
∃x φ∨ψ
φ∨∃x ψ
∀x φ∨ψ
φ∨ ∀x ψ
∃x φ∧ψ
φ∧∃x ψ
∀x φ∧ψ
φ∧∀x ψ
=>
=>
=>
=>
=>
=>
=>
=>
∃x (φ∨ψ)
∃x (φ∨ψ)
∀x (φ∨ψ)
∀x (φ∨ψ)
∃x (φ∧ψ)
∃x (φ∧ψ)
∀x (φ∧ψ)
∀x (φ∧ψ)
14
変形の手順(その4)
5. Matrix部分をCNF形式に変形する。
1. ((A∧B)∨C) を ((A∨C) ∧(B ∨C)) に
2. ((A∨B)∧C) を ((A∧C) ∨(B ∧C)) に
15
PCNF導出の例(練習問題)
x( P ( x)  P ( f ( x)))  ~ x(Q( x)  R ( x, a ))
 x(~ P ( x)  P ( f ( x)))  ~ x(Q( x)  R ( x, a ))
 x(~ P ( x)  P ( f ( x)))  ~ y (Q( y )  R ( y, a ))
 x(~ P ( x)  P ( f ( x)))  y ~ (Q( y )  R ( y, a ))
 x(~ P ( x)  P ( f ( x)))  y (~ Q( y ) ~ R ( y, a ))
 x((~ P( x)  P ( f ( x)))  y (~ Q( y ) ~ R( y, a )))
 xy ((~ P ( x)  P ( f ( x)))  (~ Q( y ) ~ R ( y, a )))
 xy ((~ P ( x)  P ( f ( x)) ~ Q( y ))  ((~ P ( x)  P ( f ( x)) ~ R ( y, a )))
何度も練習してみてください。
16
確認問題
• 次の置き換えは、真理値を保存するか
確かめよ。
D  {a, b, c}
I  {P(a, c), P(c, b), Q(a, a ), Q(a, c), Q(b, a)}
  xyP( x, y )  xQ(a, x)
  xyz ( P( x, y )  Q(a, z ))
  xy ( P( x, y )  Q(a, x))
17
確認問題
• 次の置き換えは、真理値を保存することを確
かめよ。
D  {a, b, c}
I  {P (a ), P(c)}
  xP( x)  yP ( y )
  xy ( P( x)  P( y ))
18
Skolem Standard Form
19
Skolem Standard Form
Clause
q1 x1 qn xn (C1   Cm )
Prenex
Matrix
qiはだけであり、 x1 , x2 ,, xnはすべて論理式に現れ る変数
20
PCNF => SSFへの書き換え
• 限量記号(存在記号)∃を除去しなければなら
ない。そのために、スコーレム定数やスコーレ
ム関数を導入する。
• 例:
xyP( x, y )  xP( x, f ( x))
yxP( x, y )  xP( x, a)
21
大切な注意事項(その1)
• 任意の論理式はPCNFに変形可能
• 任意のPCNFはSSFに変形可能
• 任意の論理式とそれから導かれるSSFとは
論理的に等価であるとは限らない(真理値は
必ずしも保存されない!)。
22
真理値が保存されない例
  xP( x)
  P(a)
1.D  {1,2}
2. a  2  D
3. I p (1)  T and I p (2)  F ; I  {P(1)}
大切な注意事項(その2)
• BUT
• 充足不可能な論理式は充足不可能なSSF
に変形される。
• 元の論理式がモデルを持つための必要十
分条件は、SSFがモデルを持つことである。
(これは重要な定理の1つ)
24
Herbrand Models
• 次に、フランスの論理学者Jacques Herbrand
が考案した解釈(interpretation)を導入する。
この解釈を特に、Herbrand interpretation とよ
び、この解釈に基づくモデルを Herbrand
model と呼ぶ。
25
•
•
•
•
•
Herbrand universe U
Herbrand base B
Herbrand pre-interpretation J
Herbrand interpretation I
Herbrand model M
以下、例で説明する。
26
例:
{P(a), Q(a, f (b)), x( P( x)  Q( x, x))}
まず、このような論理式
の集合を考える。
27
Herbrand Universe
U  {a, b, f (a), f (b), f ( f (a)), f ( f (b)), }
元の論理式に含まれていた定数と関数に着目し、
これからか得られるすべての項を集めたもの。
28
Herbrand Base
B  {P(a), P(b), Q(a, a), Q(b, b), P( f (a)), P( f (b)), }
元の論理式に含まれていた述語を、先ほどのUの
要素に適用して得られる述語すべてからなる集合。
29
Herbrand pre-interpretation
• 解釈の領域D:Hebrand Universe U
• 定数記号の解釈: 自分自身に対応させる。
• 関数記号の解釈:自分自身に対応させる。
30
Herbrand interpretation
• Herbrand pre-interpretation に基づく
Interpretation をHerbrand Interpretation と
呼ぶ。
• なおHIの内、所与の論理式(群)を充足する
ものを Herbrand Model (HM) と呼ぶ。
31
例
注意事項
• HMの意義
1.Σがモデルを持つ  ΣがHMを持つ。
2.Σ |= φ  SはHMを持たない。
ただし、Sは Σ∪{~φ} のSSF。
述語論理における推論
•
•
•
•
Resolution
代入
論理プログラミング(Prologなど)
帰納論理プログラミング(Progolなど)
=>知識分類・知識獲得・知識発見