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

Slides:



Advertisements
Similar presentations
1 高速フーリエ変換 (fast Fourier transform). 2 高速フーリエ変換とは? – 簡単に言うとフーリエ変換を効率よく計算 する方法 – アルゴリズムの設計技法は分割統治法に基 づいている 今回の目的は? – 多項式の積を求める問題を取り上げ、高速 フーリエ変換のアルゴリズムを用いた解法.
Advertisements

©2008 Ikuo Tahara探索 状態空間と探索木 基本的な探索アルゴリズム 横形探索と縦形探索 評価関数を利用した探索アルゴリズム 分岐限定法 山登り法 最良優先探索 A ( A* )アルゴリズム.
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
木探索によるCSPの解法 (Tree search algorithms for solving CSPs) 認知システム論 制約充足( 2 ) 制約をみたす組合せを探すエージェント バックトラック法 フォワードチェック 動的変数順序.
0章 数学基礎.
白井 良明 立命館大学情報理工学部 知能情報学科
論理による 知識の表現と推論 (Knowledge Representation and Reasoning in Logic)
第八回  シンプレックス表の経済的解釈 山梨大学.
プログラミング基礎I(再) 山元進.
プログラミング言語としてのR 情報知能学科 白井 英俊.
ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
論理による 知識の表現と推論 (Knowledge Representation and Reasoning in Logic)
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
Extremal Combinatrics Chapter 4
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
Semantics with Applications
条件式 (Conditional Expressions)
情報教育論 第9回 仮定文の仕組み 政策・メディア研究科 岡田 健.
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
9.NP完全問題とNP困難問題.
データ構造と アルゴリズム 知能情報学部 新田直也.
システム開発実験No.7        解 説       “論理式の簡略化方法”.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
10.通信路符号化手法2 (誤り検出と誤り訂正符号)
充足可能性問題SAT (Satisfiability Problem)
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
自動定理証明と応用 (automated theorem proving and its application)
命題論理 (Propositional Logic)
新ゲーム理論 第Ⅰ部 非協力ゲームの理論 第1章 非協力ゲームの戦略形
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
第4章 組合せ論理回路 (4) Quine McCluskeyの方法.
2. 論理ゲート と ブール代数 五島 正裕.
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
第25章 単一始点最短路 3節 Bellman-Fordのアルゴリズム
形式言語の理論 5. 文脈依存言語.
アルゴリズムとプログラミング (Algorithms and Programming)
執筆者:伊東 昌子 授業者:寺尾 敦 atsushi [at] si.aoyama.ac.jp
アルゴリズムとデータ構造勉強会 第6回 スレッド木
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
 型推論1(単相型) 2007.
25. Randomized Algorithms
計算量理論輪講 chap5-3 M1 高井唯史.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
書き換え型プログラムの生成・検証 研究課題:適切な実行戦略を効率よく探索する、 より自動化された手続きの実現 書き換え型プログラム
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
 型推論3(MLの多相型).
15.cons と種々のデータ構造.
5.チューリングマシンと計算.
アルゴリズムと数式の表現 コンピュータの推論
第Ⅱ部 協力ゲームの理論 第14章 交渉集合.
第7回  命題論理.
論理回路 第5回
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
4.プッシュダウンオートマトンと 文脈自由文法の等価性
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
参考:大きい要素の処理.
情報数理Ⅱ 第10章 オートマトン 平成28年12月21日.
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
アルゴリズム ~すべてのプログラムの基礎~.
練習問題.
Presentation transcript:

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

推論規則 (Inference rules)

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

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

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

命題論理の推論規則(4/5):健全な推論規則 例 モーダス・ポネンス は,健全な推論規則である. (4通りの解釈について確認せよ) 例 逆は真なり  すでに見たモーダス・ポネンスは健全な推論規則である.それを確かめるには、P, Q に与える4通りの解釈 (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 のときを考えよ)

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

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

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

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

融合原理 (Resolution principle)

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

融合原理(2):例 例 例 重複したリテラルは削除する ダメな例  例を2つ,間違いの例を1つ示す. まとめて2個キャンセルするのは,ダメ!

休憩 授業アンケート

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

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

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

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

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

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

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

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

融合原理(11):証明アルゴリズム boolean Prove (KB, Q) { OPEN ← KB∧¬Q を節集合に変換したもの. CLOSED ← { } while ( OPEN≠{ } ) { parent ← OPEN に含まれる任意の1つの節. 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および論理的帰結であることを証明したい質問Qを入力とする.数学的には,KBを公理,Qを定理ともいう.  アルゴリズムはすでに述べた考え方で空節を導出しようとする.  導出できたら true を返す.このとき, KB∧¬Q は充足不能,したがって,QはKBの論理的帰結(あるいは定理)である.  導出できなければ false を返す.このとき, KB∧¬Q は充足可能,したがって,QはKBの論理的帰結(あるいは定理)ではない. KB∧¬Q は充足可能