立命館大学 情報理工学部 知能情報学科 谷口忠大

Slides:



Advertisements
Similar presentations
立命館大学 情報理工学部 知能情報学科 谷口忠大. Information このスライドは「イラ ストで学ぶ人工知能概 論」を講義で活用した り,勉強会で利用した りするために提供され ているスライドです.イラ ストで学ぶ人工知能概 論.
Advertisements

一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
第3回 論理式と論理代数 本講義のホームページ:
第1章 数と式 第4節 集合と命題  8  集合 (第3回).
融合原理による推論 (resolution)
確率・統計Ⅰ 第11回 i.i.d.の和と大数の法則 ここです! 確率論とは 確率変数、確率分布 確率変数の独立性 / 確率変数の平均
ファジィ論理と ファジィ構造モデリング 北海道工業大学 情報デザイン学科 三田村 保.
節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
プログラミング基礎I(再) 山元進.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
演習3 最終発表 情報科学科4年 山崎孝裕.
プログラミング言語論 第4回 式の構文、式の評価
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之.
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
データ構造と アルゴリズム 知能情報学部 新田直也.
システム開発実験No.7        解 説       “論理式の簡略化方法”.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
充足可能性問題SAT (Satisfiability Problem)
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
命題論理 (Propositional Logic)
4. 組み合わせ回路の構成法 五島 正裕.
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
第4章 組合せ論理回路 (4) Quine McCluskeyの方法.
ディジタル回路 3. 組み合わせ回路 五島 正裕 2018/11/28.
2. 論理ゲート と ブール代数 五島 正裕.
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
人工知能概論 第14回 言語と論理(3) 証明と質問応答
3. 束 五島 正裕.
ディジタル回路 2. ブール代数 と 論理ゲート 五島 正裕.
第5回 今日の目標 §1.6 論理演算と論理回路 ブール代数の形式が使える 命題と論理関数の関係を示せる
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
第4回  推 論(2).
Prolog入門 ーIT中級者用ー.
 型推論1(単相型) 2007.
述語論理.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
知能情報システム特論 Introduction
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
コンパイラ 2011年10月20日
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
人工知能特論2009 No.2 東京工科大学大学院 担当教員:亀田弘之.
論理回路 第4回
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
第7回  命題論理.
東京工科大学 コンピュータサイエンス学部 亀田弘之
東京工科大学 コンピュータサイエンス学部 亀田弘之
論理回路 第5回
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
4.プッシュダウンオートマトンと 文脈自由文法の等価性
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
コンパイラ 2012年10月11日
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
練習問題.
練習問題.
Presentation transcript:

立命館大学 情報理工学部 知能情報学科 谷口忠大 人工知能概論 第13回 言語と論理(2) 記号論理 立命館大学 情報理工学部 知能情報学科 谷口忠大

Information このスライドは「イラストで学ぶ人工知能概論」を講義で活用したり,勉強会で利用したりするために提供されているスライドです.

STORY 言語と論理(2) ホイールダック2号は自然言語文を形態素解析できるようになった. 構文解析できるようになった.さて,これでスフィンクスと戦えるだろうか.そうはいかない. 単語の切れ目や,係り受け構造がわかったところでスフィンクスが「琵琶湖は湖です」「湖には水がある」といったときに,これから「琵琶湖に水がある」ということを推論することがホイールダック2号にはできない. このような文に潜む論理構造を見出すことができなければ,謎かけに答えることなどできない. ホイールダック2号に求められるのは論理的思考能力だった!

仮定 言語と論理(2) ホイールダック2号に文法に関する知識,語彙に関する知識は事前に埋め込んでよいものとする. ホイールダック2号は誤りのない音声認識が可能であるとする. ホイールダック2号は与えられた自然言語文を論理式に変換する処理系を備えているものとする.

Contents 13.1 記号論理 13.2 述語論理 13.3 節形式

自然言語の持つ「論理」の中の小さな部分! 13.1.1 記号論理 言葉で表現されるものを記号に変換したものを,その論理関係によってとらえる記号論理(Symbolic logic) 命題論理 (propositional logic) 述語論理 (predicate logic) その他多くの派生論理 様相論理,時制論理,ファジィ論理, etc. etc. 言葉で表現する物事の「真・偽」だけを論理的に扱う世界. 自然言語⊃・・・・・⊃述語論理⊃命題論理 数学の公理系⊃・・・・・・⊃述語論理⊃命題論理 自然言語の持つ「論理」の中の小さな部分!

「記号論理」の狙い 人間が行う推論を機械にやらせたい そのために、言語によらない「意味表現形式」を考案 それが記号論理   そのために、言語によらない「意味表現形式」を考案 それが記号論理 表現できる複雑さによって、 命題論理(最も簡単) 述語論理 様相論理 高階様相論理 などがある

真理値 記号論理の基本は、真理値=言葉で表現する物事の「真・偽」 例えば、この講義において は、真か偽かが決定できる  は、真か偽かが決定できる  「それぞれの文が表す内容(これを「命題」という)」には 状況(もしくは「文脈」)が与えられると真理値(真偽)が決定 教師は男性である 教師は女性である 受講生には男性しかいない 受講生には女性がいる 註:すべての命題に対し真理値が決定できるわけではない。例:「神は存在する」

論理と証明・推論 数学の証明は、「論理」によって行われる 例: 「6は素数ではない」 定義:「整数xが素数ならば、1とxだけを約数にもつ」 例: 「6は素数ではない」   定義:「整数xが素数ならば、1とxだけを約数にもつ」   この対偶: 整数xが1とx以外の約数をもてば、xは素数でない   真である命題:      6は整数である     6は1,2,3,6を約数にもつ   帰結: 6は素数ではない 基本の推論規則:モーダスポネンス 命題 A と 命題 A→B が共に真  ならば  命題 B は真 

プリンキピア・マテマティカ 数学の体系を記号論理で記述し、あらゆる数学における公理と推論規則とから数学的真理すべてを得ようとする試み ホワイトヘッドとラッセル (ともに著名な論理学者・数学者) これがもたらしたもの ゲーデルの不完全性定理 興味のある人は、『ゲーデル、エッシャー、バッハ - あるいは不思議の環』(ダグラス・ホフスタッター著、野崎昭弘、はやしはじめ、柳瀬尚紀 訳、原題は Gödel, Escher, Bach: an Eternal Golden Braid)を読んでみるとよい

Contents 13.1 記号論理 13.2 述語論理 13.3 節形式

述語論理 個々の命題の内容について論じるために,命題の中に変数を用いて,変数の値によって真・偽を捉える記号論理 命題論理では扱えない例 すべての人は平和を好む 太郎は人である. この二つから「太郎は平和を好む」を帰結する 述語論理は命題に含まれる変数に着目し,その命題における変数の性質や状態を述語(predicate)を用いて推論する.

13.2.1 記号と定義 述語記号 関数記号 定数記号 論理記号 変数記号 限量記号 述語論理は、命題論理では表せない種類の事実を記述することができる. 述語記号 関数記号 定数記号 論理記号 変数記号 限量記号

一階述語論理 本講義では「一階述語論理」を紹介 プログラミング言語の観点から、次のような見方ができる 基本の「型」は二つ 「真理値」、真True か偽False という値 「個体」、世界にある事物 述語: 一つ以上の個体を引数とし真理値を返す関数 関数: 一つ以上の個体を引数とし、個体を返す関数 論理記号: 真理値の演算、計算結果も真理値 定数: 特定の個体 変数: 「個体」型の変数

参考:高階述語論理 引数をα、値をβとする 関数の「型」 を <α, β> で表す 一階述語論理は、 述語も関数も、引数は個体に限定 これを「一階」という 述語: <個体 (,…,個体), 真理値> 関数: <個体 (,…,個体), 個体> 二階述語論理は、 一階述語論理の関数や述語を引数とする 関数や述語を認める 二階述語: <<個体,真理値>,真理値> 二階関数: <<個体,真理値>,個体>

一階 述語論理で用いる記号(1)

一階 述語論理で用いる記号(2)

項の定義 原子論理式の定義 定数記号,変数記号はすべて項である. 個体に対応 定数記号,変数記号はすべて項である. t1, t2, . . . , tn が項であり,f が関数記号であるとき f(t1, t2, . . . , tn)も項である. 原子論理式の定義 t1, t2, . . . , tn が項であり,pが述語記号であるとき,p(t1, t2, . . . , tn)を原子論理式(atomic formula) という. 真理値に対応

述語論理式の定義 原子論理式は論理式である. 真理値に対応 --- 原子論理式が「単文」ならこれは「一般の文(複文含む)」 原子論理式は論理式である. P,Qが論理式であれば,論理記号を用いて構成される¬P(否定), P ∧ Q(連言), P ∨ Q(選言), P → Q(含意), P ≡ Q(同値) も論理式である. P が論理式で,x が個体変数であるとき,∀xP, ∃xP は論理式である. 上記より論理式となるものだけが論理式である.

論理式を解釈する(interpretation) 論理式の真偽は,その論理式を構成している原子論理式の真偽をそれぞれ求め,それらの論理記号による結びつきを考え,元となる論理式全体の真偽を決定する. 1 = TRUE 0 = FALSE

演習13-1 下の真理値表を完成させよ.(T=1, F=0) p q ¬p∨q p→q ¬(q→p) p∧¬p T F

恒真式,恒偽式 原子論理式のとる真理値にかかわらず,常に真であるものや常に偽であるものが存在する. 恒真式 (tautology)・・・解釈によらず真 トートロジー 恒偽式 (contradiction)・・・解釈によらず偽 矛盾式 充足可能 (satisfiable)・・・解釈次第で真 充足不能 (unsatistiable)・・・解釈によらず偽 同じ

矛盾式(コントラディクション)と恒真式(トートロジー) 「僕は君を愛してもおり,愛していなくもある. ああ,僕のこの想いをどう言葉にすればいいんだ・・メリッサ!」 「世の中には二種類の人間が居る.寿司を愛するものと,寿司を愛さないものだ.寿司こそ全てだよ!」 矛盾: p∧¬p 意味不明 恒真: p∨¬p あたりまえだから 何の情報もない

論理式の同値関係 二重否定 ¬(¬p)≡p べき等律 p∨p≡p, p∧p≡p 補元律 p∨¬p≡T, p∧¬p≡F 二重否定 ¬(¬p)≡p べき等律 p∨p≡p, p∧p≡p 補元律 p∨¬p≡T, p∧¬p≡F 交換律 p∨q≡q∨p, p∧q≡q∧p 結合律 (p∧q)∧r≡p∧(q∧r),(p∨q)∨r≡p∨(q∨r) 分配律 p∨(q∧r)≡(p∨q)∧(p∨r),    p ∧(q ∨ r)≡(p ∧ q) ∨(p ∧ r) ド・モルガン律 ¬(p∧q)≡¬p∨¬q,  ¬(p∨q)≡¬p∧¬q 恒真,恒偽 p∨T≡T,p∧T≡p, p∨F≡p,p∧F≡F, 含意の除去 p→q≡¬p∨q 同値記号の除去  (p≡q)≡((p→q)∧(q→p))

13.2.3 述語論理式の例 (教科書 表13.3) 別解 ∃x(have(I, x) ∧ (book(x) ∨ notebook(x))

演習13-2 先に挙げた例, をそれぞれ,述語論理式であらわしてみよう. 何をどのように変数と置くかは自分で考えてみよう. p1 すべての人は平和を好む p2 太郎は人である. p3 太郎は平和を好む. をそれぞれ,述語論理式であらわしてみよう. 何をどのように変数と置くかは自分で考えてみよう.

Contents 13.1 記号論理 13.2 述語論理 13.3 節形式

13.3.1 命題論理式の節形式への変形 命題論理式 基礎となる原子論理式がP,Q,R などの記号でおかれ,これらを上記五つの論理記号で結合することによって得られる論理式 同値となる論理式は多数あるために,標準形を定めておくことは都合が良い.(多項式における因数分解,展開に近い) 連言標準形(和積標準形:conjunctive normal form) リテラル (literal) ・・素式,または素式の否定 節 (close)・・・リテラルの論理和のみからなる論理式 節形式 (closed form) ・・・節の論理積のみからなる論理式 リテラル 節 節形式

命題論理式の連言標準形への変形

論理式の節形式への変換 step1 同値記号≡と含意記号→を以下の同値関係を用いて除去する. p≡qは,((p→q)∧(q→p))と同値 p→q≡¬p∨q step2 二重否定,ド・モルガン律を適用する. ¬(¬p)≡p ¬(p∧q)≡¬p∨¬q,  ¬(p∨q)≡¬p∧¬q step 3 分配律を適用する. p∨(q∧r)≡(p∨q)∧(p∨r), p ∧(q ∨ r)≡(p ∧ q) ∨(p ∧ r)

教科書の例 P ≡ Q ∨ R 手で追ってみよう...

演習問題 13-3 次の命題論理式を連言標準形の節形式に変換しなさい. (p→q)∧(¬p→¬(q∨r))

13.3.2 述語論理のスコーレム標準形への変形 スコーレム標準形 スコーレム関数を用いて存在記号∃を除去した節形式なので,スコーレム標準形と言われる.

スコーレム標準形への変形例(1) ¬(∀xp(x)) ≡ ∃x(¬p(x)) ¬(∃xp(x)) ≡ ∀x(¬p(x)) 同値と含意の除去 二重否定の除去とド・モルガンの法則による否定記号の移動 限量記号のド・モルガンの法則 ¬(∀xp(x)) ≡ ∃x(¬p(x)) ¬(∃xp(x)) ≡ ∀x(¬p(x))

スコーレム標準形への変形例(2) 変数の標準化 スコーレム関数を用いた存在記号の除去 冠頭形への変形 分配律を用いて節形式へ変形 各節の変数の独立化 ⇒

13.3.3 節集合 スコーレム標準形による節形式は必ず以下の形をとる. ∀x1,.... ,∀ xn (C1∧ C2 .... ∧ Cn) 節集合形式での記述 C={C1, C2 ,.... , Cn} 母式( matrix) 述語論理式は 節の集合で表せば十分!

演習13-4 次の述語論理式のスコーレム標準形を求め,節集合形式で表しなさい. ∀x∃y[P(x)→Q(x,y)]∧¬(∀x∃y[P(x)∧∀zR(z)])

まとめ 述語論理で用いる記号を導入し述語論理の基礎について学んだ. 恒真式,恒偽式とは何かについて学び,主要な同値関係について確認した. 事実を表す一般的な自然文を一階述語論理式として表現する方法を学んだ. 命題論理式の節形式への変形方法について学んだ. 述語論理式のスコーレム標準形および節集合形式への変形方法について学んだ.

予習問題 1.図14.3において、空節が導かれると、なぜ、 P→Q と P∧R から Q∧R が証明できたといえるのか、説明してみよう 2.「太郎は暇なら、太郎はゲームをしている」、「太郎は暇だ」、「花子は勉強している」ということから、「太郎はゲームをしており、花子は勉強している」が、導出原理により証明できだろうか? 3.太郎の子は一太郎、一太郎の子は健一郎、子供の子供は孫、を前提としたとき、太郎の孫が誰かを導出原理を用いて答えられるか?