人工知能特論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の例 xy (( P( x) ~ Q( x, y )) (~ R(a, b) ~ P(a ))) xyz ( 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 )) xy (~ 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 ))) xy ((~ P ( x) P ( f ( x))) (~ Q( y ) ~ R ( y, a ))) xy ((~ 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)} xyP( x, y ) xQ(a, x) xyz ( P( x, y ) Q(a, z )) xy ( P( x, y ) Q(a, x)) 17 確認問題 • 次の置き換えは、真理値を保存することを確 かめよ。 D {a, b, c} I {P (a ), P(c)} xP( x) yP ( y ) xy ( 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への書き換え • 限量記号(存在記号)∃を除去しなければなら ない。そのために、スコーレム定数やスコーレ ム関数を導入する。 • 例: xyP( x, y ) xP( x, f ( x)) yxP( 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など) =>知識分類・知識獲得・知識発見
© Copyright 2024 ExpyDoc