数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.

Slides:



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

一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
0章 数学基礎.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
融合原理による推論 (resolution)
近似アルゴリズム 第10章 終了時刻最小化スケジューリング
ファジィ論理と ファジィ構造モデリング 北海道工業大学 情報デザイン学科 三田村 保.
計算の理論 II 帰納的関数(つづき) 月曜4校時 大月美佳.
計算の理論 I 決定性有限オートマトン(DFA) と 非決定性有限オートマトン(NFA)
Extremal Combinatorics 14.1 ~ 14.2
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
8.クラスNPと多項式時間帰着.
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
立命館大学 情報理工学部 知能情報学科 谷口忠大
人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之.
Semantics with Applications
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
充足可能性問題SAT (Satisfiability Problem)
離散数学I 第6回 茨城大学工学部 佐々木稔.
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
自動定理証明と応用 (automated theorem proving and its application)
第2章 「有限オートマトン」.
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
形式言語とオートマトン Formal Languages and Automata 第4日目
3. 可制御性・可観測性.
第25章 単一始点最短路 3節 Bellman-Fordのアルゴリズム
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
人工知能概論 第14回 言語と論理(3) 証明と質問応答
形式言語の理論 5. 文脈依存言語.
計算の理論 II 帰納的関数 月曜4校時 大月美佳.
計算の理論 II 帰納的関数2 月曜4校時 大月美佳.
形式言語とオートマトン Formal Languages and Automata 第4日目
7.4 Two General Settings D3 杉原堅也.
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
述語論理.
25. Randomized Algorithms
Structural operational semantics
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
計算の理論 II 前期の復習 -有限オートマトン-
知能情報システム特論 Introduction
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
知識表現 知識の表現形式 宣言的表現 手続き的表現 プロダクション・ルール フレーム 意味ネットワーク.
論理回路 第4回
行列式 方程式の解 Cramerの公式 余因数展開.
第7回  命題論理.
論理回路 第5回
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
4.プッシュダウンオートマトンと 文脈自由文法の等価性
計算の理論 I NFAとDFAの等価性 火曜3校時 大月 美佳 平成16年5月18日 佐賀大学理工学部知能情報システム学科.
計算の理論 I 反復補題 火曜3校時 大月 美佳 平成16年7月13日 佐賀大学知能情報システム学科.
計算の理論 I ε-動作を含むNFA 火曜3校時 大月 美佳 平成16年5月25日 佐賀大学知能情報システム学科.
形式言語とオートマトン Formal Languages and Automata 第5日目
計算の理論 I ー ε-動作を含むNFA ー 月曜3校時 大月 美佳.
計算の理論 II 多テープTuring機械 月曜4校時 大月美佳 平成16年11月29日 佐賀大学知能情報システム学科.
立命館大学 情報理工学部 知能情報学科 谷口忠大
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
練習問題.
練習問題.
Presentation transcript:

数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔

前回までのあらすじ http://sas.cis.ibaraki.ac.jp/logic/ 述語論理と導出原理 単一化置換 単一化アルゴリズム ファクタリング 配布資料は以下のURLからダウンロードできます http://sas.cis.ibaraki.ac.jp/logic/

前回の問題 以下の文を考える。 「花子」は「松夫」の母親である。 「花子」は「太郎」の妻である。 「z」は「y」の父親である。 このとき、以下の導出節を単一化して、「誰」が「誰」の父親であるか答えなさい。 {母親(花子, 松夫), 妻(花子, 太郎),  ~母親(x, y)∨~妻(x,z)∨父親(z,y)}

前回の問題 {母親(花子, 松夫), 妻(花子, 太郎), ~母親(x, y)∨~妻(x,z)∨父親(z,y)} 母親(花子, 松夫)と母親(x, y)で単一化を行う。 不一致集合は{‘花子’=x, ‘松夫’=y} となるため、 x=‘花子’, y=‘松夫’ として単一化する。 妻(花子, 太郎)と妻(花子,z)で単一化を行う。 不一致集合は{‘太郎’=z} となるため、 z=‘太郎’ として単一化する。 その結果、父親(太郎, 松夫) となるので、 「太郎は松夫の父親である。」 となる。

今週のお題 述語論理と導出原理 エルブランの定理 導出原理 述語表現と推論

エルブランの定理 節集合 C の充足不能性を調べる 必要な知識 エルブラン領域 基礎列、エルブラン基底 エルブラン解釈

エルブラン領域 項が取り得る値の範囲 エルブラン領域 H の求め方 充足不能を調べる領域と等価なひとつの領域 i = 0, 1, 2, ・・・ について、 Hi+1 = Hi ∪{f(t1, t2, ・・・, tn)の集合} f は節集合に現れるすべての関数 t1, t2, ・・・, tn は Hi のすべての要素

エルブラン領域を求める例 C={P(x, a),Q(b, f(y))} のエルブラン領域 H0 = {a, b} H1 = {a, b, f(a), f(b)} H2 = {a, b, f(a), f(b), f(f(a)), f(f(b))}   ・・・ H = {a, b, f(a), f(b), f(f(a)), f(f(b)), f(f(f(a))), f(f(f(b))), ・・・}

基礎節 基礎節 エルブラン基底 HB(C) エルブラン解釈 節集合の各変数にエルブラン領域の要素を代入 P(a, a), Q(b, f(a)), P(b, a), Q(b, f(b)) エルブラン基底 HB(C) 基礎節のすべての集合 HB(C) = {P(a, a), Q(b, f(a)), P(b, a), Q(b, f(b)), P(f(a), a), Q(b, f(f(a))), ・・・} エルブラン解釈 エルブラン基底の各要素に真偽を割り当てたもの

エルブランの定理 エルブラン基底 エルブラン解釈 真となるエルブラン解釈がひとつでも存在 HB = {A1, A2, ・・・, Ai, ・・・} エルブラン解釈 HI1 = { A1,  A2, A3, ・・・} HI2 = {~A1,  A2, A3, ・・・} HI3 = { A1, ~A2, A3, ・・・} HI4 = {~A1, ~A2, A3, ・・・} 真となるエルブラン解釈がひとつでも存在 充足可能

エルブラン解釈 A1 ~A1 A2 ~A2 A2 ~A2 A3 ~A3 A3 ~A3 A3 ~A3 A3 ~A3 HI1 HI3 HI2

エルブランの定理 節集合 C が充足不能であるとき、そしてそのときに限り、意味木はすべての順路で偽となる節点に到達する

ひとつのエルブラン解釈の意味木 F F ~T∨F =F {~P(a)∨Q(f(a)), P(a), ~Q(f(a))} P(a) ~P(a)

導出原理 恒偽性を証明すべき節集合 C 中の2つの節 Ci, Cj を単一化 上の処理を繰り返す C = {C1, C2, ・・・, Cn} 導出節 Cij が空節ならば充足不能、 導出節 Cij が空節でなければ C に追加 上の処理を繰り返す 充足不能であれば空節が導出できる

導出原理の例 論理式 この論理式の節集合 この節集合から結論 ∃xC(x) を反駁定理で証明 ∃x(A(x)∧∀y(A(y)⇒B(x)))∧(∀xB(x)⇒C(x)) この論理式の節集合 {A(a), ~A(y)∨B(a), ~B(x)∨C(x)} この節集合から結論 ∃xC(x) を反駁定理で証明

導出原理の例 結論 ∃xC(x) の否定 空節を求めるべき節集合は以下になる 単一化を行いながら導出木により空節を導く ~∃xC(x) = ∀x~C(x) 空節を求めるべき節集合は以下になる {A(a), ~A(y)∨B(a), ~B(x)∨C(x), ~C(x)} 単一化を行いながら導出木により空節を導く

反駁導出による証明 □ A(a) ~A(y)∨B(a) B(a) ~B(x)∨C(x) C(a) ~C(x) [ y = a ] [ x = a ] C(a) ~C(x) [ x = a ] □ 矛盾するため、 ∃xC(x) は成り立つ (証明終わり)

述語表現と推論 ペアノの公理(自然数についての規則) 次の式を満たす集合 N 1∈N x∈N ならば、σ(x)∈N x≠y ならば、σ(x)≠σ(y) x∈N ならば、σ(x)≠1 N の部分集合 S が以下を満たすとき、 S=N 1∈S x∈S ならば、σ(x)∈S

ペアノの公理 述語により記述 N(x) : x は自然数である S(x) : x は集合 S の要素である EQ(x, y) : x と y は同じである s(x) : σ(x)

ペアノの公理(述語論理版) N(1) ∀xN(x) ⇒ N(s(x)) ∀x∀y(~EQ(x, y) ⇒ ~EQ(s(x), s(y))) ∀x(N(x) ⇒ ~EQ(s(x), 1)) ∀x(S(x)⇒N(x))∧(S(1)∧∀x(S(x) ⇒S(s(x)))⇒∀y(S(y)⇔N(y)))

自然数の加算 次の数を表す関数 s(x) 加算(x+y=z)を表す述語 Plus(x, y, z) s(0)=1, s(s(0))=2, s(s(s(0)))=3, ・・・ s(s(・・・s(0))) = n 加算(x+y=z)を表す述語 Plus(x, y, z) Plus(x, y, z) を関数 s を用いて定義 n 個

自然数の加算 以下の式を仮定 2+3を計算 0+x=x x+y=z ⇒ (x+1)+y=(z+1) 結論 Plus(0, x, x) Plus(x, y, z) ⇒ Plus(s(x), y, s(z)) 2+3を計算 結論 ∃xPlus(s(s(0)), s(s(s(0))), x)

加算の定義と結論から得られる節集合 {Plus(0, x, x),                  ~Plus(x, y, z)∨Plus(s(x), y, s(z)), ~Plus(s(s(0)), s(s(s(0))), x) }

~Plus(x1, y1, z1) ∨ Plus(s(x1), y1, s(z1)) ~Plus(s(s(0)), s(s(s(0))), x) [x1 = s(0), y1 = s(s(s(0))), x = s(z1) ] ~Plus(x2, y2, z2) ∨ Plus(s(x2), y2, s(z2)) ~Plus(s(0), s(s(s(0))), z1) [x2 = 0, y2 = s(s(s(0))), z1 = s(z2) ] ~Plus(0, s(s(s(0))), z2)

導出の続き (空節) ~Plus(0, s(s(s(0))), z2) Plus(0, x3, x3) [x3 = s(s(s(0))), z2 = s(s(s(0))) ] (空節)

x には何が代入されているの? x = s(z1) z1 = s(z2) z2 = s(s(s(0))) よって、 x= s(z1) = s(s(z2)) = s(s(s(s(s(0)))))

練習問題 節集合{~F(x)∨G(x), ~G(a)}から、∃x~F(x)を証明せよ。 論理式 Plus(0, x, x)、 Plus(x, y, z) ⇒ Plus(s(x), y, s(z)) から、1+1の計算を行う論理式 ∃xPlus(s(0), s(0), x) を証明し、xに入る値を求めよ。 節集合{~F(x)∨G(x), ~G(a)}から、∃x~F(x)を証明せよ。