融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す

Slides:



Advertisements
Similar presentations
1 線形代数学. 2 履修にあたって 電子情報システム学科 必修 2005 年度1セメスタ開講 担当 草苅良至 (電子情報システム学科) 教官室: G I 511 内線: 2095 質問等は上記のいずれかに行なうこと。 注意計算用のノートを準備すること。
Advertisements

論理回路 第 11 回
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
0章 数学基礎.
区間グラフにおける区間表現からMPQ-treeを効率よく構成するアルゴリズム
第3回 論理式と論理代数 本講義のホームページ:
論理による 知識の表現と推論 (Knowledge Representation and Reasoning in Logic)
第八回  シンプレックス表の経済的解釈 山梨大学.
融合原理による推論 (resolution)
© Yukiko Abe 2014 All rights reserved
確率・統計Ⅰ 第11回 i.i.d.の和と大数の法則 ここです! 確率論とは 確率変数、確率分布 確率変数の独立性 / 確率変数の平均
節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換
論理による 知識の表現と推論 (Knowledge Representation and Reasoning in Logic)
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
Extremal Combinatorics 14.1 ~ 14.2
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
    有限幾何学        第5回.
プログラミング言語論 第4回 式の構文、式の評価
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
立命館大学 情報理工学部 知能情報学科 谷口忠大
人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之.
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
Semantics with Applications
情報教育論 第9回 仮定文の仕組み 政策・メディア研究科 岡田 健.
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
9.NP完全問題とNP困難問題.
データ構造と アルゴリズム 知能情報学部 新田直也.
Probabilistic Method 6-3,4
システム開発実験No.7        解 説       “論理式の簡略化方法”.
最尤推定によるロジスティック回帰 対数尤度関数の最大化.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
10.通信路符号化手法2 (誤り検出と誤り訂正符号)
基本情報技術概論(第3回) 埼玉大学 理工学研究科 堀山 貴史
充足可能性問題SAT (Satisfiability Problem)
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
自動定理証明と応用 (automated theorem proving and its application)
命題論理 (Propositional Logic)
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
第4章 組合せ論理回路 (4) Quine McCluskeyの方法.
2. 論理ゲート と ブール代数 五島 正裕.
形式言語の理論 5. 文脈依存言語.
ディジタル回路 2. ブール代数 と 論理ゲート 五島 正裕.
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
第4回  推 論(2).
古代の難問と曲線 (3時間目) 筑波大学大学院 教育研究科 1年                 石井寿一.
 型推論1(単相型) 2007.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
人工知能特論2009 No.2 東京工科大学大学院 担当教員:亀田弘之.
基本情報技術概論(第2回) 埼玉大学 理工学研究科 堀山 貴史
論理回路 第4回
  第3章 論理回路  コンピュータでは,データを2進数の0と1で表現している.この2つの値,すなわち,2値で扱われるデータを論理データという.論理データの計算・判断・記憶は論理回路により実現される.  コンピュータのハードウェアは,基本的に論理回路で作られている。              論理積回路.
    有限幾何学        第5回.
アルゴリズムと数式の表現 コンピュータの推論
計算の理論 I ー正則表現とFAの等価性ー 月曜3校時 大月 美佳.
第7回  命題論理.
論理回路 第5回
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
4.プッシュダウンオートマトンと 文脈自由文法の等価性
情報処理Ⅱ 2005年10月28日(金).
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
情報数理Ⅱ 第10章 オートマトン 平成28年12月21日.
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
練習問題.
Presentation transcript:

融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す 人工知能 論理と推論(2) 知識を組み合わせて知識を生み出す 融合原理 (resolution)  論理的帰結  節形式  融合原理  今回の授業では,命題論理の「節形式」と呼ばれる論理式で記述された複数の知識が与えられたとして,それらを組み合わせて「推論」することによって,既に知られている知識から論理的に帰結される新しい知識を生成する「融合原理」と呼ばれるアルゴリズムを学ぶ.

論理的帰結 (logical consequence) 論理的帰結(1):論理的帰結の定義 論理的帰結 (logical consequence) が真となるどんな解釈によっても が真のとき, の論理的帰結  は であるといい,つぎのように書く.  「論理的帰結」の定義については,前回の授業でも触れたが,今回は特にこの概念が重要となるので,その復習からスタートする.  論理式は,そこに含まれる変数の「解釈」(「真」と考えるか「偽」と考えるか)によって,全体として真であったり偽であったりすることを思い出そう.そこで,論理式PとQが与えられたとして,Pを真とする解釈をすべて列挙してみる.それらのうちのどの解釈を用いても,必ずQも真であるとき,「QはPの論理的帰結」であるという.このスライドでは,このようなPがn個与えられるような一般的な状況において,この「論理的帰結」の定義を拡張したものを示している. という前提が成り立つときには, という結論も成り立つことが確実に言えるということ.

論理的帰結(2):真理値表による論理的帰結の判定 例 解釈 前提 結論 P Q P→Q P∨Q T F  例として,このスライドにある3つの論理式    PならばQ, PまたはQ, Q を考え,「Q」が「PならばQ」及び「PまたはQ」の論理的帰結であることを確認しよう.  変数はPとQなので,可能な解釈は,このスライドの真理値表の4つの行に対応するある4通りがある.前回学んだ「ならば」と「または」の意味計算の方法によって計算すると, 「PならばQ」と「PまたはQ」という2つの前提を共に真(T)とする解釈は,この表のように,1つ目の解釈(P=Q=T)と3つ目の解釈(P=F,Q=T)である.この2つのいずれの解釈のもとでも,結論を表す論理式「Q」は真である.したがって,定義により,「Q」は「PならばQ」及び「PまたはQ」の論理的帰結であることがわかる. 前提が真となるすべての解釈 のもとで結論も真

論理的帰結(3):演習問題 前提1 暑くて湿度が高ければ,雨が降るだろう. 前提2 湿度が高いのに暑くないということはあり得ない. 前提3 いま,湿度が高い.  演習問題:このスライドに書かれた3つの前提が成り立つとすれば,「雨が降るだろう」という命題は,その論理的帰結となることを示そう.まず,記号化をする.  P=「暑い」  Q=「湿度が高い」  R=「雨が降るだろう」 という変数を導入すると,3つの前提及び結論を表す命題は,スライドに示した論理式として記号化できる.  つぎに,「論理的帰結」の定義にしたがって,前提を真とするすべての解釈を求めよう.変数が3つあるので,可能な解釈は最大で8つある.しかし,前提3が「Q」という単純な形であることから,少なくともQ=Tであるような解釈だけに限ればよいので,最大でも4つにしぼられる.ここから先は宿題である. 論理的帰結 雨が降るだろう. ヒント:解釈は8通りあるが,QがFである解釈は考える必要なし.     残りの4通りを考察する.

論理的帰結(4):論理的帰結と充足不能の関係 背理法 の論理的帰結  は 同値 は充足不能(矛盾)   「論理的帰結」という概念は,前回学んだ「充足不能(矛盾)」という概念と密接に関係している.それを示したのがこのスライドである.これは,一般に,数学において「背理法」と呼ばれる証明手法の根拠となっている.つまり,「結論Qは前提Pの論理的帰結である」という定理を証明するために,「前提Pが成り立ち,かつ,結論の否定が成り立つ」という命題は決して成り立たない(充足不能),すなわち,この命題は矛盾を含むことを証明するのである.

論理的帰結(5):例 例 同値 は充足不能 解釈 前提 結論の否定 P Q P→Q P∨Q ¬Q T F  先ほどの例を,いま説明した「背理法」の考え方で解いてみよう.  前提である「PならばQ」及び「PまたはQ」は成り立つとして,それに加えて,結論「Q」の否定「Qでない」が成り立つであろうか?  この真理値表からわかるように,可能な4つの解釈のいずれによっても,これら3つの論理式の少なくとも1つが偽(赤く示してある)であることがわかる.つまり,この3つの論理式が同時に成り立つことは絶対ない.したがって,それらの論理積(AND)は必ず偽となる.よって,この3つの論理式の論理積は充足不能である.ゆえに,一つ前に示したスライドの関係によって,「Q」は「PならばQ」及び「PまたはQ」の論理的帰結であると言うことができる.

復習 節形式(1):節形式への変換 節: リテラルの選言. 節形式: 節の連言. 節形式への変換 1 2 3 4 ド・モルガンの法則 5 復習 節形式(1):節形式への変換 節: リテラルの選言. 節形式: 節の連言. どんな論理式も以下の変換ルール(左辺を右辺に書換え)で 等価な節形式に変換できる. 節形式への変換 1 2  これは「節形式」の復習.  「変数」,または,「変数の否定」を「リテラル」という.  「節」は「リテラル」の論理和である.  「節形式」は「節」の論理積である.  どのような論理式もここで示した方法によって,論理的に等価な節形式に変形することができる. 3 4 ド・モルガンの法則 5 分配則 6

復習 節形式(2) :節形式への変換 例 節形式 したがって,つぎの2つの節が得られる. 節集合 復習 節形式(2) :節形式への変換 例 節形式  節形式からAND記号を除去して,節を集めたものが「節集合」である. したがって,つぎの2つの節が得られる. 節集合

融合原理(1) 融合原理 つぎの (1) (2) 式より (3) を導出する推論規則 融合節  これが今回の授業の山場,「融合原理」の説明図である.  2つの論理式(1),(2)が与えられたとしよう.さらに,(1)の一部には変数Pが含まれていて,(2)の一部にはその否定(not P)が含まれているとする.(この2つのリテラル(Pとnot P) は,実際には,このスライドのように左端に現われている必要はない.節はリテラルをORで結合したものであり,ORはその結合の順番を変えたり入れ換えたりしても等価だからである.  このような状況になっているとき,(1)からPを除去し,(2)からnot Pを除去して,残りのリテラルをORで結合したものは,やはり,節の形をしている.これを融合節と呼び,(3)と番号を付けよう.  このように,(1)と(2)から融合節(3)を生成するアルゴリズムを融合原理という.Pを正リテラル,not Pを負リテラルという.この正負のことをリテラルの符号という.この言葉を使って表現すると,融合原理とは,2つの節から符号だけが異なるリテラルを1個ずつキャンセル(削除)し,残りのリテラルをORで結合するアルゴリズムであるということができる. 符号の異なるリテラルを1個ずつキャンセルし, 残りのリテラルを結合する.

融合原理(2):例 例 モーダス・ポネンス(Modus Ponens) 例 対偶  前回の授業で説明したような,よく知られる推論規則も融合原理によって説明できる.  たとえば,モーダス・ポネンスは,スライドの右半面に書かれているように,「P」及び「PならばQ」という2つの前提から,「Q」という結論が導かれることを表している.この問題に対して融合原理を使うと,「P」及び(「PならばQ」を節形式で表した)「not P またはQ」からPとnot Pをキャンセルして「Q」を導くことができる.  対偶についても同様である.

融合原理(3):例 例 三段論法 例 例 空節(矛盾)  その他,いろいろな推論規則を融合原理によって統一的に説明することができる.融合原理とは,それほど強力なアルゴリズムなのである.これだけ知っていればあとは知らなくとも良いとさえ言えそうである. 空節(矛盾)

休憩

融合原理(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と節not Pに融合原理を適用することによってできる,1つもリテラルを含まないような節である.Pとnot Pから作られることからもわかるように,これは「矛盾」を表している.健全性によって,もともとの節集合が真ならば,導出された節も真であることが保証されているのだが,空節は「偽」であり,絶対に真ではない.したがって,融合原理によって空節が生成されたということは,もともとの節集合が決して真には成り得ない,すなわち,その節集合は充足不能であることを表している.  「完全性」というのは,その逆を表している性質である.節集合が充足不能ならば,必ずその節集合から空節を導き出すことができる.

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

融合原理(8):例題 例 同値 は充足不能 先ほどの例を融合原理を用いて証明したのが,このスライドである.  先ほどの例を融合原理を用いて証明したのが,このスライドである.  この図は「融合木」と呼ばれるグラフ構造を表している.木のノードは与えられた節集合に含まれている節,または,それらから融合原理によって導出された節を表している.融合原理で用いた2つの節(親)とそこから生成された融合節(子)とを辺で結んでいる.  最終的に空節(□)が生成されたので,与えられた節集合は充足不能であることがわかる.したがって,「Q」は「PならばQ」及び「PまたはQ」の論理的帰結であることがわかった.

融合原理(9):例題 前提1 暑くて湿度が高ければ, 雨が降るだろう. 前提2 湿度が高いのに暑くない ということはあり得ない. 前提3  すでに述べたこの例題も融合原理で解いてみよう.そのために,前提を表すすべての論理式を節形式に変換する.また,結論を表す論理式は否定した後に節形式に変換する. 前提3 いま,湿度が高い. 否定 論理的帰結 雨が降るだろう.

融合原理(10):例題 前提 結論の否定  この融合木からわかるように,空節が生成されたので,問題で与えられた3つの前提が成り立つならば,その論理的帰結として,「雨が降るだろう」ということを結論としてよいことがわかる.