人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之.

Slides:



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

一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
0章 数学基礎.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
融合原理による推論 (resolution)
法とコンピュータ 法的知識の構造(3) 慶應義塾大学法学部 2008/11/25 吉野一.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
8.クラスNPと多項式時間帰着.
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
立命館大学 情報理工学部 知能情報学科 谷口忠大
Natural Semantics 実行過程の、最初と最後の状態(state)の関係を考える。
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
9.NP完全問題とNP困難問題.
「情報数学06前再」の注意事項 このページの内容は  「情報数学06前再」(3単位)を履修している諸君には上田先生からの連絡が届きます。 「06前再」の受講者は,情報理工学科の「情報数学」
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
10.通信路符号化手法2 (誤り検出と誤り訂正符号)
充足可能性問題SAT (Satisfiability Problem)
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
人工知能特論2007 東京工科大学 亀田弘之.
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
ディジタル回路 3. 組み合わせ回路 五島 正裕 2018/11/28.
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
プログラミング言語論 第3回 BNF記法について(演習付き)
計算の理論 II NP完全 月曜5校時 大月美佳 平成17年1月17日 佐賀大学理工学部知能情報システム学科.
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
人工知能概論 第14回 言語と論理(3) 証明と質問応答
執筆者:伊東 昌子 授業者:寺尾 敦 atsushi [at] si.aoyama.ac.jp
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
Prolog入門 ーIT中級者用ー.
Where is Wumpus Propositional logic (cont…) Reasoning where is wumpus
「情報数学06前再」の注意事項 このページの内容は 
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
(1)序論 人工知能とは 歴史 方法論 人工知能の基礎 問題解決 探索 推論 知識.
知能情報システム特論 Introduction
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
第5章 計算とプログラム 本章で説明すること ・計算の概観と記述法 ・代表的な計算モデル ・プログラムとプログラム言語.
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
東京工科大学 コンピュータサイエンス学部 亀田弘之
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
 型推論3(MLの多相型).
人工知能特論2009 No.2 東京工科大学大学院 担当教員:亀田弘之.
論理回路 第4回
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
Prolog入門 ーIT中級者用ー.
第7回  命題論理.
東京工科大学 コンピュータサイエンス学部 亀田弘之
東京工科大学 コンピュータサイエンス学部 亀田弘之
論理回路 第5回
プログラミング言語論 第10回 情報工学科 篠埜 功.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
再履修の諸君への連絡事項 このページの内容は 
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
4.プッシュダウンオートマトンと 文脈自由文法の等価性
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
東京工科大学 コンピュータサイエンス学部 亀田弘之
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
練習問題.
練習問題.
Presentation transcript:

人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之

命題論理(Propositional Logic) 命題論理では、自然言語の文を単純化・ 形式化し、その枠組みで推理等を整理・ 体系化することを目指す。 例(推理の例): 泳げば、濡れる。(If P, then R.) シャワーをかかれば濡れる。(If Q, then R.) → 泳ぐかシャワーをかかれば濡れる。 (If P or Q, then R.)

命題論理の体系(概要) syntax(文法) semantics 記号の並びに関する規約(well-formed) 論理式とはどんな形式のものなのか。 semantics Well-formed な論理式相互の関係 真・偽

Syntax どのような形式言語にもシンタックスがある。 例: プログラミング言語(Java, C, Prolog etc.) XML (eXtensible Markup Language) HTML (HyperText Markup Language) UML (Unified Modeling Language) UNL (Universal Networking Language) etc.

定義3.1 命題論理の字母は以下の記号からなる。 アトム記号(atom)の集合A(非空集合) A ={ P, Q, R, … , P1, P2, …, Q1, Q2, …} 結合子(connectives): ~, ∧, ∨, →, ↔ 補助記号(右括弧と左括弧): (, )

定義3.1のコメント 命題論理はすでに述べたように、形式化された文に対して定義される。対象となる文は何らかの記号の列であり、その記号を 字母(alphabet)として定義している。 字母として {あ, い, う, …, あ1, あ2, あ3,…, い1,…, not, and, or, then, eq, [, ] } を採用してもよい。表現には自由度があるが論理体系としては同一である。

定義3.2 (well-formedな)論理式 (Well-formedな)論理式(formula)とは 以下のようなものである。 アトムは論理式。 ( if P ∈ A , then P is formula.) φが論理式ならば、~φは論理式。 φとψが論理式ならば、 (φ∧ψ), (φ∨ψ), (φ→ψ), (φ↔ψ) は論理式。

定義3.2のコメント 任意のアトムPは論理式(原始式ともいう) アトムではない論理式、例えば、~Pや(P→Q)は複合論理式ともいう。 Pがアトムのとき、Pと~Pをリテラル(literal)と呼ぶ。特に、Pを正リテラル(positive literal)、~Pを負リテラル(negative literal)と呼ぶ。

論理式の例 P (P∧Q) ~((P3∧P8)∨~Q2) ((P∨Q)→R) (P→(P→P)) (~P↔(~(Q∧P)))

問題:論理式でない例を3つ挙げよ。

定義3.3 命題論理言語 命題論理言語(propositional language)とは、所与の字母から構成される論理式全体の集合のことをいう。

定義3.3のコメント 定義3.1と定義3.2から得られる記号列全体のこと。 この場合、「記号列=論理式」である。 論理式は「形式文」ともみなせるので、 命題論理言語という言い方をする。

Semantics 文=論理式 には意味を与えることができる。 論理学ではまずは 「真と偽」を考える。 (「真・偽」以外は後日考察する。)  (「真・偽」以外は後日考察する。) 今の段階では、∧や ~ は単なる記号であり、論理積や論理否定の意味はまだ導入されていない点に注意。これからそれらを導入する。

定義3.4 解釈 Intp 命題論理言語 L に対し、Lのアトムの集合をA とする。このとき、L の解釈 Intp とは、A から{T, F}への写像のことをいう。 ここで、TとFを真理値と呼ぶ。    解釈Intp: A → { T, F }

定義3.5 解釈の表現法 解釈 Intp はアトム A の集合の部分集合として記述することとする。 つまり、 Intp = { x | Intp(x) = T, x∈A }

解釈の例 A = { P, Q, R }において、 Intp(P)=T, Intp(Q)=T, Intp(R)=F のとき、これを Intp = { P, Q } と書く。また。 Intp(P)=T, Intp(Q)=F, Intp(R)=F のときは、 Intp = { P } と書く。

定義3.6 結合子の意味の定義 表.結合子の定義表 P Q ~P (P∧Q) (P∨Q) (P→Q) (P↔Q) T F 定義3.6 結合子の意味の定義 表.結合子の定義表 P Q ~P (P∧Q) (P∨Q) (P→Q) (P↔Q) T F これは真理値表である。

定義3.7  φを論理式、Intpを1つの解釈とする。 このとき、もしφの真理値がIntpのもとで T であれば、 「φは解釈Intpのもとで真である」 あるいは 「解釈Intpはφを満たす(満足する)」 という。

例 φ=~(P∧Q), Intp={P} のとき、 φの真理値はTとなるので、φはIntpのもとで真であり、Intpはφを満足する。

定義3.8 モデル φを論理式、Intpを解釈とする。このとき、Intpがφを満足するならば、「Intpはφのモデルである」という。また、「φはIntpをモデルとしてもつ」ともいう。

例 φ=((P∧Q)↔(R→Q)) Intp = { P, R } このとき、Intpはφのモデルである。 (各自確認せよ。)

定義3.9 モデル(その2) 論理式の集合をΣ、Intpを解釈とする。このとき、Σに属するどの論理式に対してもIntpがそのモデルになっているとき、「IntpはΣのモデルである」という。

例 Σ= { P, (Q∨R), (Q→R) } Intp1 = { P, R } Intp2 = { P, Q, R } Intp3 = { P, Q } このとき、Intp1とIntp2はΣのモデルであるが、Intp3はΣのモデルではない。 (各自確認せよ。)

定義3.10 論理的帰結 Σ:論理式の集合 φ:論理式 定義3.10 論理的帰結 Σ:論理式の集合 φ:論理式  このとき、Σのどのモデルもまたφのモデルになっているとき、「φはΣの論理的帰結(logical consequence)である」といい、   Σ |= φ と書く。また、「Σは論理的にφを含意する」などともいう。

定義3.11 論理的帰結(その2) Σ,Γ:論理式の集合 このとき、Σのどのモデルも論理式φ∈Γの モデルとなっているとき、「ΣはΓのモデルである」といい、Σ |= Γ と書き、また、「ΣはΓを論理的に含意する」という。

例 P = “私は外にいる” Q = “雨が降っている” R = “私は濡れる” このとき、    ( (P∧Q) → R ) かつ Q から    ( P → R ) が結論付けられる。

つまり ( (P∧Q) → R ) , Q |= ( P → R ) (この証明は次の通り)

P Q R ((P∧Q)→R) (P→R) T F 解釈1 解釈2 解釈3 解釈4 解釈5 解釈6 解釈7 解釈8

つまり ( (P∧Q) → R ) , Q |= ( P → R ) (この証明は次の通り) これのモデルは、1,2,5,6の4つ。 これのモデルは、解釈2以外の解釈。 解釈1,5,6は これのモデル でもある。 これらに共通のモデルは、1,5,6の3つ。 (この証明は次の通り)

練習問題 Σ={(P∧Q), (P→R)} は Γ= {P,Q,R} を含意する、すなわち、Σ|=Γ であることを示せ。

定理3.1 演繹定理 Σ|=(φ→ψ) のとき、またそのときに限り、Σ∪{φ} |= ψ である。

証明 Σ∪{φ} |= ψ  Σ∪{φ} のどのモデルもψのモデル  Σのどのモデルも~φかψのモデル  Σのどのモデルも(φ→ψ)のモデル  Σ |= (φ→ψ)

定義3.12 論理的に等価(⇔) 論理式φとψは、 φ |= ψ と ψ |= φ とがともに成り立つとき、「φとψは論理的に等価である」といい、「φ⇔ψ」と書く。

定義3.13 論理的に等価(その2) 論理式の集合ΣとΓが論理的に等価であるとは、以下の条件が成り立つことを言い、 Σ⇔Γ と書く。 Σ |= Γ かつ Γ |=Σ

例 Σ = { P, ~Q, (P∨R)} , Γ = { (R∨P), (~R∨~Q), P, (P→~Q)} のとき、 Σ⇔Γである。 (各自証明せよ。)

定義3.14.1 φのどの解釈もφのモデルになっているとき、φは妥当(valid)であるといい、また、φは恒真式(tautology)であるという。 このとき、 |= φ と書く。

定義3.14.2 φの解釈の中にモデルが存在するとき、φは充足可能(satisfiable)である、あるいは、無矛盾(consistent)であるという。

定義3.14.3 φの解釈の中に1つもモデルが存在しないとき、φは充足不可能(unsatisfiable)である、あるいは、矛盾(inconsistent)であるという。

定義3.14.4 充足可能な論理式のうち、恒真式(ト-トロジ)でないものをcontigentという。

論理式の分類 Contigent 矛盾 Tautology 真のこともあれば偽のこともある 常に偽 常に真 充足不可能 充足可能

例(トートロジの例) (P∨~P) ( ( P∧(P→Q) ) → Q )  (各自で例を考えよ。)

命題3.1 Σ |= φ iff Σ∪{~φ} が充足不可能。 ただし、 Σ:論理式の集合 φ:論理式 (注) iff とはif and only if の略記法で、A iff B とは、AとBが同値であることを意味する。

証明 Σ |=φ iff φはΣのどのモデルに対しても真 iff Σ∪{~φ} はモデルを持たない iff Σ∪{~φ} は充足不可能

ここまでは前回の復習

論理式の標準形(Normal Form) 論理積標準形 論理和標準形 conjunctive normal form (CNF) disjunctive normal form (DNF)

定義3.15 論理和/積標準形 Aijをリテラルとするとき、 ∨∧Aij の形の論理式を論理和標準形といい、 ∧∨Aij の形の論理式を論理積標準形という。

例(論理和標準形) (P∧Q ∧ R)∨(~P ∧ Q ∧ R) ∨(P ∧ Q ∧ ~R) (注)論理回路のときには、 P・Q・R + ~P・Q・R + P・Q・~R    などと書いていた。

例(論理積標準形) (P∨~Q)∧(P∨~R)  (P + ~Q)・(P + ~R)

定理3.2 標準形の存在 任意の論理式 φ に対して、それと等価な CNF と DNF が存在する。   (証明は各自に任せます。)

そこで、例えば論理式(P∨~Q)∧(P∨~R) を { {P, ~Q}, {P, ~R} } などと書くことにする。 これ以降、論理式は CNF で考える。 そこで、例えば論理式(P∨~Q)∧(P∨~R) を { {P, ~Q}, {P, ~R} } などと書くことにする。 (P∨~Q)∧(P∨~R)  の別表記法として                { {P, ~Q}, {P, ~R} } を導入する。 この表現方法に 慣れてください。

練習問題 { ~P, Q} { {P, Q, ~R}, {~P,Q} } { {P, R}, {~P, ~R} }

定義3.16 節と節集合 節とはゼロ個以上の リテラルの並び のこと。 { P, Q, ~R } などと標記する。 定義3.16 節と節集合 節とはゼロ個以上の リテラルの並び のこと。 { P, Q, ~R } などと標記する。 節集合とは、節の集合のこと。

例 節: 節集合: { P, ~Q } { } (空節) { P1, Q3, R } { } (空節) { P1, Q3, R } 節集合: { { P, ~Q }, { }, { P1, Q3, R } }

Horn節とHorn節集合 高々(at most)1つの正リテラルしか持たない節の ことをHorn節という。 例: F=(P∨~Q)∧(~R∨~P∨S)∧(~P∨~Q)∧S∧~U F={ {P,~Q}, {~R,~P,S}, {~P,~Q}, {S}, {~U} }

例: G=(P∨~Q)∧(R∨~P∨S) G={ {P,~Q}, {R,~P,S} } (これはHorn節集合ではない)

導出原理(Resolution法)

定義 リテラルの相補性 リテラルAとBが相補的であるとは、 A=~B であるか B=~A であることである。 また、Aと相補的なリテラルをA*と書く。

定義 導出節(resolvent) 2つの節C1とC2に対して、C1に属する1つのリテラルAの相補的リテラルA*がC2に属しているとする。 このとき、 節(C1ー{A})∪(C2ー{A*}) をC1とC2からの導出節(resolvent)と呼ぶ。

定義 導出原理 2つの節から導出節を作り出すことを 導出原理という。 また、この操作による推論法をresolution法と呼ぶこととする。

導出原理の意味 {~P, Q}, {P} から {Q} を作り出す(導く)のが導出原理法であり、これは、いわゆる三段論法(modus ponens)に相当するものである。

練習問題 導出節をすべて求めよ。 { {A,~B,E}, {A,B,C}, {~A,~D,E},{A,~C} } (注)アトムとしてA,B,C,D,Eという記号を    用いた。今後は適宜さまざまな記号を    用いることとする。

答え(後日掲載します)

Lemma K1とK2が節集合Fの要素(節)であるとする。このとき、もしRがK1とK2の導出節ならば、F∪{R} はFと論理的に同値である。 すなわち、 F∪{R}  F 証明は各自で挑戦してみてください。

定義 Res(F) Res(F) = F∪{ R | R はFからの導出節} Res0(F) = F Resn+1(F) = Res(Resn(F)) for n≧0 Res*(F) = ∪Resn(F)

練習問題 Resn(F) (n=0,1,2) をそれぞれ求めよ。 ただし、 F={ {A,~B,C}, {B,C}, {~A,C}, {B,~C}, {~C} }

Resolution定理 節集合Fに対して、Fが充足不可能であることと、□∈Res*(F) であることとは同値である。 F is unsatisfiable    □∈Res*(F) .

推論とは 推論(inference)とは、いくつかの命題(論理式)からなる前提(premise)から、1つの 命題(論理式)を結論(conclusion)として導き出す過程のこと。例えば、 彼はギリシア人かインド人である。 彼がギリシア人ならば彼はギリシア語を話せる。 彼はギリシア語を話せない。 したがって、 彼はインド人である。 前 提 結 論

分析 P = 彼はギリシア人である Q = 彼はインド人である R = 彼はギリシア語を話せる とすると、 (P∨Q)∧(P→R)∧~R 故に、Q

(P∨Q) (P→R) ~R ---------------------------------- Q

この推論の正しさを示すためには、前提がすべて真のとき結論も真であることを示せばよい。つまり、 この推論の正しさを示すためには、前提がすべて真のとき結論も真であることを示せばよい。つまり、 (P∨Q)∧(P→R)∧~R |= Q が成り立つことを示せばよい。

そこでまずは、… Resolution法の妥当性を確認しよう! {~P, Q}, {P} |= Q  (~P∨Q)∧P |= Q P Q F

Resolution法を用いた証明方法 Σ |= φ を証明するには、 Σ∪{~φ} |= □ を示せばよい。 Σ |= φ を証明するには、 Σ∪{~φ} |= □ を示せばよい。 (演繹定理とResolution定理より。) つまり、前提であるΣに証明したいφの否定を追加すると矛盾が生じることを示せばよい。(いわゆる“背理法”。)

証明: (P∨Q)∧(P→R)∧~R |= Q これにresolution法を適用する。 (次のスライド参照)

{ {P,Q}, {~P,R}, {~R}, {~Q} } {P,Q} {~P,R} {~R} {~Q} {P} {~P} □

問題:次の推論は正しいか? 山田か田中が参加できれば、この企画は成功する。 山田が海外に出張中であれば、山田はこの企画に参加できない。 田中も忙しければ、この企画に参加できない。 山田は海外に出張中であるが、田中は忙しくない。 故に、この企画は成功する。

P=山田はこの会議に参加できる Q=田中はこの会議に参加できる R=この会議は成功する S=山田は海外出張中である T=田中は忙しい (P∨Q)→R, S→~P, T→~Q, S∧~T |= R

(P∨Q)→R, S→~P, T→~Q, S∧~T |= R

((~P∨R)∧(~Q∨R))∧(~S∨~P)∧(~T∨~Q)∧S∧~T |= R

(~P∨R)∧(~Q∨R)∧(~S∨~P)∧(~T∨~Q)∧S∧~T ∧ ~R これから、 Res*(F) を求めるとこの中には□が含まれない。 ということは、この推論は誤っている。 (真理値表を書いて確認せよ。)

練習問題 次の論理式はトートロジであることを示せ。 F=(~B∧~C∧D)∨(~B∧~D) ∨(C∧D)∨B

練習問題 F = A∧B∧C が次の論理式の帰結であることを示せ。( G |= F ) G={{~A,B},{~B,C},{A,~C},{A,B,C}}

推論の完全性・健全性

今後の予定 述語論理の導入 ユニフィケーション 述語論理における導出原理 など 述語論理のシンタックス 述語論理のセマンティックス 標準形(冠頭標準形) ユニフィケーション 述語論理における導出原理 など

参考文献 ライプニッツの哲学 ー 論理と言語を中心に ー, 石黒, 岩波書店(1984). Beginning Logic, E.J.Lemmon, Chapman & Hall/CRC(1965). 情報科学における論理,小野寛晰,日本評論社(1994). 1は言語哲学の本です。論理学をより深く学ぶ場合、一度目を通しておくとよいと思います。2は論理学の古典的名著の1つです。日本語訳もあります。 3は皆さんのような人たちの学習参考書です。