融合原理による推論 (resolution)

Presentation on theme: "融合原理による推論 (resolution)"— Presentation transcript:

1 融合原理による推論 (resolution)
認知システム論　知識と推論（３） 知識と論理で問題を解決する 融合原理による推論 (resolution) 　推論規則 　融合原理 　今回の授業では，命題論理の節集合によって記述された複数の知識が与えられたとして，それらを組み合わせて「推論」することによって，既に知られている知識から論理的に帰結される新しい知識を生成する「融合」（レゾリューション）と呼ばれる推論アルゴリズムを学ぶ．

2 推論規則 (Inference rules)

3 命題論理の推論規則（1/5）：推論規則とは？
前提 推論規則 結論 前提がすべて知識ベース（ＫＢ）に入っていたら， 結論をＫＢに追加してよい． KB KB 　推論規則とは，スライドのように，一見，分数のように見える形式で表現される．横線の上にある論理式を前提，横線の下にある論理式を結論という．いま、いろいろな知識が論理式の形式で知識ベース（ＫＢ）に格納されているとしよう。推論規則の意味は，「前提がすべてＫＢに入っていたら，結論をＫＢに追加してよい」ということである．これにより，ＫＢの状態が遷移することになる． 状態遷移

4 命題論理の推論規則（2/5）：モーダス・ポネンス
P, Q はKB内の論理式（命題）そのものではなく，それらを値としてとる変数（命題変数）を表している． KB KB Glitter→Gold Glitter→Gold Glitter 　実際には，推論規則内に書かれている変数は，KB内の論理式（命題）そのものではなく，それらを値としてとる変数（命題変数）を表している．たとえば，スライドに書かれている「モーダス・ポネンス」という推論規則は，「ＫＢ内に知識Ｐおよび知識Ｐ→Ｑが含まれていれば，知識ＱをＫＢに追加してよい」という意味だが，実際には，このスライドにあるように，知識 Glitter と知識 Glitter→Gold から知識 Gold を推論するために使うことができる． Glitter Gold 輝くものは黄金である． それは輝いている． それは黄金である．

5 命題論理の推論規則（3/5）：健全性 推論規則 は， を満たすとき，健全であるという． の論理的帰結 は のすべてを真とする
の論理的帰結　 は 　推論規則は，その結論が前提の論理的帰結であるとき，健全であるという．すなわち，その前提がすべて真であるときに，結論もまた必ず（いかなる解釈によっても）真であるということである． のすべてを真とする どんな解釈のもとでも が真

6 命題論理の推論規則（4/5）：健全な推論規則
例 モーダス・ポネンス は，健全な推論規則である． （４通りの解釈について確認せよ） 例 逆は真なり 　すでに見たモーダス・ポネンスは健全な推論規則である．それを確かめるには、P, Q に与える４通りの解釈 (P,Q) =(T,T),(T,F),(F,T),(F,F)のそれぞれについて、前提P, P→Q がTならば、結論QもまたTであることを確認すればよい．実際、前提P, P→Q がTである解釈は(P,Q) =(T,T)のみであり、このとき確かにQ=Tとなる． 　「逆は真なり」は健全な推論規則ではない．P=F, Q=T という解釈を考えると，前提 P→Q はTだが，結論Q→PはFだからである． は，健全ではない． （逆は真とは限らぬ．P =F，Q =T のときを考えよ）

7 命題論理の推論規則（5/5）：その他の推論規則
以下の推論規則は，いずれも健全である 対偶 三段論法 ∧導入 ∧除去 ∨導入 ∨除去 　この授業では，健全な推論規則のみに興味がある．このスライドに示す６つの推論規則は，いずれも健全である．この他にも健全な推論規則は，たくさんある．

8 例題 魔宮の世界 背景知識 (1,2) にモンスターがいるなら，(1,1) で異臭を感じる
例題　魔宮の世界 背景知識 (1,2) にモンスターがいるなら，(1,1) で異臭を感じる (1,2) に落とし穴があるなら，(1,1) で風を感じる (1,2) にモンスターも落とし穴もないなら，(1,2) はOK 事実 質問 (1,1) で異臭を感じない (1,2) はOKか？ 　前回導入した「魔宮の世界」の例題を考えてみよう．(1)～(5)の知識がＫＢに含まれているとき，OK12がその論理的帰結かどうか調べたい．これは，結論の否定 ¬OK12 をＫＢに追加したとき，ＫＢが充足不能であることと等価であったことを思い出してほしい．（背理法の原理と同じ．） (1,1) で風を感じない と仮定し，充足不能であれば OK

9 例題 魔宮の世界：推論規則による判定 対偶：(1)より ＭＰ：(4),(7)より 対偶：(2)より ＭＰ：(5),(9)より
例題　魔宮の世界：推論規則による判定 証明 対偶：(1)より ＭＰ：(4),(7)より 対偶：(2)より MPは モーダス・ポネンス の略 ＭＰ：(5),(9)より ∧導入：(8),(10)より 　前回の授業では，この問題を制約充足問題の一種である充足可能性問題と見て，バックトラック法によってすべての論理式を真とする解釈（すなわち，各変数にtrue/false のどれを割り当てると全体が真となるか）を探索して，そのような解釈が存在しないことを確認することによって，充足不能であることを判定した．今回は，推論規則を用いて判定してみよう． 　このスライドにあるように，健全な推論規則を適切に用いることによって，空節が導出された．空節は「常にfalse」すなわち「矛盾」を表している．したがって，背理法の考え方と同様に，結論 OK12 が知識ベース　{(1),(2),(3),(4),(5)}　の論理的帰結であることが証明された．（このような論理式の列 (1),…,(13) を証明という．） ＭＰ： (11),(3)より ∨除去： (6),(12)より □ ゆえに，充足不能 空節（矛盾）

10 疑問点と問題点 推論規則は，あれだけで十分か？ もっと多く必要か？ もっと少なくてよいか？ 適用可能な推論が多すぎて，探索効率が悪い ∨導入
もっと多く必要か？　もっと少なくてよいか？ 適用可能な推論が多すぎて，探索効率が悪い ∨導入 　ここで，疑問点と問題点が明らかとなる． 　疑問点は，「推論規則は，あれだけで十分か」ということである．他にもいろいろなことを証明したいとき，他にもっと推論規則が必要になるのではないだろうか？　あるいは，逆に，これほどたくさんの推論規則がなくても，十分ではないだろうか？ 　問題点は，「適用可能な推論が多すぎて，探索効率が悪い」ことである．たとえば，「∨導入」という推論規則は，P という知識があるときに，任意の論理式Qを用いて，P∨Q という知識を作り出す．これでは，コンピュータによって自動的に証明を作り出そうとするときには，証明に必要とされない論理式をたくさん生成する必要が生じ，明らかに効率が悪い． 　以下では，その解答を示す．結論を言えば，「融合」というただ１つの推論規則だけあれば十分である．融合は，すでに示した「∨導入」などの推論規則より，はるかに無駄な論理式の生成を抑制できて効率が良いのである． 融合というただ１つの推論規則だけあれば十分である．

11 融合原理 (Resolution principle)

12 融合原理（1） 融 合 (resolution) 節に対して適用する推論規則 CとDは節 融合節 融合節
符号の異なるリテラルを１個ずつキャンセルし， 残りのリテラルを∨で結合する． 　これが「融合」（レゾリューション）の説明図である． 　２つの論理式 　　　Ｐ∨Ｃ　(1) 　　　￢Ｐ∨Ｄ　(2) が与えられたとしよう．(1)の一部には変数Pが含まれていて，(2)の一部にはその否定( ￢Ｐ）が含まれている．この２つのリテラル（Ｐと￢ P） は，実際には，このスライドのように左端に現われている必要はない．節はリテラルを∨ で結合したものであり， ∨は交換則と結合則により，その結合の順番を変えたり入れ換えたりしても等価だからである．Ｃは(1)の中に含まれるＰ以外のリテラルを∨で結合したもの（節）である．Ｄは(2)の中に含まれる￢Ｐ以外のリテラルを∨で結合したもの（節）である． 　このような状況になっているとき，(1)からＰを除去し，(2)から ￢Pを除去して，残りのリテラルを∨で結合したもの 　　　Ｃ∨Ｄ　(3) は，やはり，節の形をしている．これを(1),(2)から得た融合節と呼ぶ． 　このように，(1)と(2)から融合節(3)を生成する推論規則を融合（レゾリューション）という．Pを正リテラル，￢Pを負リテラルという．この正負のことをリテラルの符号という．この言葉を使って表現すると，融合とは，２つの節から符号だけが異なるリテラルを１個ずつキャンセル（削除）し，残りのリテラルを∨ で結合する推論規則であるということができる． 　なお，融合節が Q ∨Q ∨Sのように，重複したリテラル（この例ではQ）を持つことがある．そのときは，１個だけを残して，他は削除する．なぜならば，論理和の性質により，x ∨x = x だからである． キャンセルするリテラルの節の中の場所はどこでもよい． （左端である必要はない） 重複したリテラルは１個を残して削除する．

13 融合原理（2）：例 例 例 重複したリテラルは削除する ダメな例 　例を２つ，間違いの例を１つ示す． まとめて２個キャンセルするのは，ダメ！

14 休憩 授業アンケート

15 融合原理（3）：例 例 モーダス・ポネンス 例 三段論法 例 矛盾 空節 よく知られる推論規則も融合原理によって説明できる．
　よく知られる推論規則も融合原理によって説明できる． 　たとえば，モーダス・ポネンスは，スライドの右半面に書かれているように，Ｐ及びＰ→Ｑという２つの前提から，Ｑという結論が導かれることを表している．この問題に対して融合原理を使うと，Ｐ及び（Ｐ→Ｑを節形式で表した）￢P∨ＱからPと￢PをキャンセルしてＱを導くことができる． 　三段論法についても同様である． 　簡単だが，重要な例として， ￢PとPから空節が導かれることを覚えておこう．空節は常に偽である節なので，矛盾を表している． それは，￢PとPが互いに相容れないことを表していることからも明らかである． 例 矛盾 空節

16 融合原理（4）：導出と導出可能性 導出と導出可能性 節集合 に次々と融合を適用し， 節の系列 が得られるとき， から が導き出される
という． また， から へ導出可能といい， とかく． 　節集合が与えられたとき，次々と融合を適用し，節が次々と生成されていく．生成された節は，最初の節集合から導き出された（あるいは導出された）ものであるという．

17 融合原理（5）：健全性 P = F の場合： P = T の場合： 定理 任意の２つの節 Ｃ１，Ｃ２ の融合節 Ｃ は
Ｃ１，Ｃ２ の論理的帰結になっている． 証明 Ｃ１，Ｃ２ を T とする解釈を考える． P = F の場合： P = T の場合： 　融合の理論的に重要な性質として，「健全性」と「完全性」がある． 　健全性とは，融合節(3)はその親である(1),(2)の節の論理的帰結になっていることをいう．つまり，融合によって生成される節はでたらめなものではなく，すでに知られている知識（節）から論理的・必然的に成立するものだけが生成されるのである． 　健全性は，融合のワンステップだけで成り立つのではなく，何ステップに渡っても成り立つ．つまり，融合によって導出された論理式は，すべて最初の節集合の論理的帰結になっている． 健全性：導出したものは論理的帰結になっている． ならば

18 融合原理（6）：完全性 健全性の別な言い方： 節集合 S から空節 □ が導き出されれば， S は充足不能である． 逆 定理 完全性
　融合によって，空節が導き出されたとしよう．空節というのは，節Ｐと節￢Pに融合を適用することによってできる，１つもリテラルを含まないような節である．Ｐと￢ Pから作られることからもわかるように，これは「矛盾」を表している．健全性によって，もともとの節集合が真ならば，導出された節も真であることが保証されているのだが，空節は「偽」であり，絶対に真ではない．したがって，融合原理によって空節が生成されたということは，もともとの節集合が決して真には成り得ない，すなわち，その節集合は充足不能であることを表している． 　「完全性」というのは，その逆を表している性質である．節集合が充足不能ならば，必ずその節集合から空節を導き出すことができる．この分野の多くの応用では，節集合が充足不能であることを証明することを要求する．節集合が充足不能の場合，融合を用いて必ず空節を導き出すことができるのである．逆に，空節を決して導き出せないことがわかれば，もともとの節集合は充足可能である．

19 融合原理（7）：融合原理を用いた証明 の論理的帰結 は 同値 は充足不能 同値 は充足不能 節集合 同値 から空節を導出可能
の論理的帰結　 は 同値 は充足不能　 同値 は充足不能　 節集合 同値 　これまでの理論をまとめると，このスライドのようになる． 　「ＱがＰの論理的帰結である」ということを証明するのが目標である．そのためには，Ｐ∧￢ Qが充足不能であることを証明すればよい．そのためには，その論理式Ｐ∧￢ Q を節集合Ｓに変換し，融合によって空節を導出すればよいのである． 　健全性によって，空節が導出されれば，ＱがＰの論理的帰結であることを結論してよい． 　逆に，ＱがＰの論理的帰結ならば，完全性によって，実際，必ず空節を導出することができるのである． 　この過程はすべてコンピュータによって全自動で行うことができる．（論理式を節形式に自動変換する処理と，２つの節を系統的に組み合わせて融合節を生成する処理が中心となる．） から空節を導出可能　

20 融合原理（8）：例題 魔宮の世界 知識ベース 結論の否定 結論の否定 (1),(4)より (2),(5)より (3),(6)より
融合原理（8）：例題　魔宮の世界 知識ベース 結論の否定 結論の否定 (1),(4)より (2),(5)より (3),(6)より 　魔宮の世界の例題をこの考え方で解いてみた． (8),(9)より (7),(10)より 矛盾

21 融合原理（9）：例題 魔宮の世界：証明の探索
融合原理（9）：例題　魔宮の世界：証明の探索 (1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) 　実際には，証明で必要とされない多くの節が生成され得ることに注意しよう．１つまえのスライドに示した　(7)から(11)までの節は，証明に必要な節だけを抜き書きしたものである． 証明に不必要な節もたくさん導出されている 効率向上のための工夫が必要

22 融合原理（10）：証明の探索の制御 初期状態 CLOSEDは空リスト．すべての節を OPENに． CLOSED LIST OPEN LIST
一般の状態 CLOSEDリスト内のどの２つの節も融合済み C C C C parent 各Ｃと融合 導出節をOPENに追加 　コンピュータによって自動的に空節を導出するプログラムを作るには，２つの節に融合を組織的に適用して，できるだけ無駄なく推論を進めるコントロールが必要である．その基本的な考え方をスライドに示す． 　その考え方は，探索アルゴリズムに似ている．最初は，ＫＢおよび結論の否定から得られるすべての節をOPENリストに登録し，CLOSEDリストを空にする． 　アルゴリズムは，OPENから１つの節を取り出し，CLOSEDに移動する．そして，その節とCLOSED内の各節との融合を試み，生成された融合節のうち，初めて見たもの（CLOSEDにもOPENにも含まれていないもの）をOPENに登録する．このようなコントロールによって，CLOSED内のどの２つの節の組合せも，すでに融合を試みた対とすることができる．したがって，OPENの中の節とCLOSEDの中の節との組合せだけを考えれば良いのである．ちなみに，OPENの中の節どうしの組合せも必要だが，このアルゴリズムでは，OPENから選ばれた節がすぐにCLOSEDに移動するので，結局， OPENとCLOSEDの間の組合せだけに帰着されるのである． child

23 融合原理（11）：証明アルゴリズム boolean Prove (KB, Q) { OPEN ← KB∧¬Q を節集合に変換したもの．
CLOSED ← { } while ( OPEN≠{ } ) { parent ← OPEN に含まれる任意の１つの節． OPENから parent を削除する． for each clause C in CLOSED do { children ← parent と Cからのすべての導出節の集合． 　　　　 if ( □∈children ) return true 　　　　　 childrenに含まれる節のうち，OPENにもCLOSEDにも 　　　　　　　　　　　　　　　　　含まれないものをOPENに追加する． } 　　return false // KB: 知識ベース（公理），　Q: 質問（定理） KB∧¬Q は充足不能 　この考え方をアルゴリズムとしてまとめる．この関数は，知識ベースKBおよび論理的帰結であることを証明したい質問Ｑを入力とする．数学的には，ＫＢを公理，Ｑを定理ともいう． 　アルゴリズムはすでに述べた考え方で空節を導出しようとする． 　導出できたら true を返す．このとき， KB∧¬Q は充足不能，したがって，ＱはKBの論理的帰結（あるいは定理）である． 　導出できなければ false を返す．このとき， KB∧¬Q は充足可能，したがって，ＱはKBの論理的帰結（あるいは定理）ではない． KB∧¬Q は充足可能