節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換

Slides:



Advertisements
Similar presentations
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
Advertisements

0章 数学基礎.
和田俊和 資料保存場所 /2/26 文法と言語 ー正規表現とオートマトンー 和田俊和 資料保存場所
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
融合原理による推論 (resolution)
プログラミング言語としてのR 情報知能学科 白井 英俊.
近似アルゴリズム 第10章 終了時刻最小化スケジューリング
実証分析の手順 経済データ解析 2011年度.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
演習3 最終発表 情報科学科4年 山崎孝裕.
情報とコンピュータ 静岡大学工学部 安藤和敏
統率・束縛理論2.
プログラミング言語論 第4回 式の構文、式の評価
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
立命館大学 情報理工学部 知能情報学科 谷口忠大
条件式 (Conditional Expressions)
数理論理学 第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)
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
第4章 組合せ論理回路 (4) Quine McCluskeyの方法.
3. 可制御性・可観測性.
識別子の命名支援を目的とした動詞-目的語関係の辞書構築
PROGRAMMING IN HASKELL
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
形式言語の理論 5. 文脈依存言語.
6.2.4 辞書項目(1) 辞書項目にも、語に対するDAGを与える。
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
 型推論1(単相型) 2007.
述語論理.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
様々な情報源(4章).
知能情報システム特論 Introduction
情報処理Ⅱ 第2回:2003年10月14日(火).
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
SUNFLOWER B4 岡田翔太.
コンパイラ 2011年10月20日
融合原理 (resolution) 人工知能 論理と推論(2) 論理的帰結 節形式 融合原理 知識を組み合わせて知識を生み出す
 型推論3(MLの多相型).
モデル検査(5) CTLモデル検査アルゴリズム
曲がった時空上の場の理論の熱的な性質と二次元CFT
  第3章 論理回路  コンピュータでは,データを2進数の0と1で表現している.この2つの値,すなわち,2値で扱われるデータを論理データという.論理データの計算・判断・記憶は論理回路により実現される.  コンピュータのハードウェアは,基本的に論理回路で作られている。              論理積回路.
第7回  命題論理.
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第10回 情報工学科 篠埜 功.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
矛盾した知識 デフォルト推論 仮説を用いた推論 準無矛盾推論 デフォルト規則 デフォルト理論の拡張 → デフォルト証明 シナリオ
4.プッシュダウンオートマトンと 文脈自由文法の等価性
情報処理Ⅱ 2005年10月28日(金).
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
コンパイラ 2012年10月11日
情報とコンピュータ 静岡大学工学部 安藤和敏
PROGRAMMING IN HASKELL
情報数理Ⅱ 第10章 オートマトン 平成28年12月21日.
情報処理Ⅱ 小テスト 2005年2月1日(火).
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
Presentation transcript:

節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換 認知システム論 知識と推論(5) 知識と論理で問題を解決する 節集合 (set of clauses) 一階述語論理による知識表現の技法 節集合への変換

復習(1/3) 個体記号 個体記号 オブジェクト(個体)を表現 A 述語記号 (1変数) オブジェクトの性質(property)を命題として表現 Mortal A is mortal. A 述語記号 (2変数) オブジェクト間の関係(relation)を命題として表現 A is a friend of B. A B 関数記号 オブジェクト間の関数(function)を表現 名前の ない要素 A father of A

復習(2/3) 項 原子式

復習(3/3) 限量子: 全称記号 「すべての x について」 (for all x , …) 存在記号「ある x が存在して」 限量子:   全称記号 「すべての x について」 (for all x , …) All 存在記号「ある x が存在して」 (there exists x such that …) Exists

述語論理による知識表現の技法

表現の技法(1/9) 定義域 定義域(オブジェクトの世界)を決定する D = {Jack, Elizabeth,...} :いろいろな人の集合 D = {0, 2, π,1+2i, ...} : すべての数の集合  ここまでで,一階述語論理の構文論と意味論という形式的な理論は学んだことになるが,実際問題としては,与えられた知識をいかにして記号的に表現するかということは,基本的には人間が行うべき仕事である.この仕事は,案外むずかしい.しかし,一階述語論理は論理的な「言語」なので,我々の使う日本語や英語などの自然言語(特に,「論理」発祥の地であるギリシャの流れをもつヨーロッパ系の言語)との関連を理解すると,表現のコツがつかめてくる.  まず,いろいろな概念や事物を4種類のどの記号で表現したらよいかを考えておこう.その場合,各記号には「解釈」を通して意味を付与することとなるが,その解釈の基盤となる定義域Dを事前に具体的に決定しておく必要がある.

表現の技法(2/9) 個体記号(定数) 固有名詞,数詞は個体記号(定数)で表現 Jack, Mickey,Sapporo 2, π 点P,直線L,三角形ABC  このスライドでは,個体記号(定数)で表現すべきものの例を示している.個体記号は定義域D内の個別の要素を表すものなので,固有名詞や数詞など,個々のオブジェクトを表すものは,個体記号(定数)で表すのが自然である.

表現の技法(3/9) 述語記号 普通名詞,形容詞,動詞は述語記号で表現 DOCTOR(x): x is a doctor. INT(x): x is an integer. RED(x): x is red. GREATER(x, y): x is greater than y. ON(x, y): Point x lies on Line y. LOVES(x, y): x loves y. PRODUCT(x, y, z): The product of x and y is z.  「述語記号」の「述語」という言葉は,主語・述語というときの「述語」のことであり,英語の文法的には動詞や(be動詞+)形容詞がそれにあたる.そのほか,普通名詞も述語記号にするとうまくいくことが多い.  動詞は主語や目的語などと共に用いられる用法が決まっているので,それに応じた変数(引数)の数をもつ述語記号にする.たとえば,love という動詞は,S loves O のように「主語+loves+目的語」で使用されるので,2変数の述語記号LOVESを導入して LOVES(S, O) のように記述する.  形容詞は,「主語+be動詞+形容詞」の形で用いられ,主語の性質を表すので,主語を引数とする1変数述語記号にすることが多い.たとえば,S is red は RED(S) のように表現される.  普通名詞(たとえば,「医師」)というのは,特定の個人や事物を表しているものではなく,各個人あるいは事物の性質(属性,プロパティ)を表しているものなので,すでに学んだ意味論での議論によると,それは命題(たとえば,「○○は医師である」)を表すための述語記号を導入するのが良いのである.たとえば,S is a doctor は DOCTOR(S) あるいは IS-DOCTOR(S) などのように表現される.

表現の技法(4/9) 関数記号 MOTHER(x, y): y is the mother of x. 2変数以上の述語で1つの引数が他の引数から 一意に決定できる MOTHER(x, y): y is the mother of x. SUCCESSOR(x, y): y is the successor of x (y=x+1). MID(x, y, z): z is the midpoint of x and y. 関数記号で表すことも可能 the 普通名詞 of は関数記号で表現 mother(x): the mother of x s(x): the successor of x (= x + 1) mid(x, y): the midpoint of x and y  2変数以上の述語で,1つの引数が他の引数から一意に決定できる場合には,関数記号を用いても良い.その指針は,英語の「the + 普通名詞 + of 」のような定冠詞(the)を用いた表現によって,特定の事物から一意に定まるオブジェクトを表しているかどうかである.たとえば,mother(x) は「xの母」を表す.どの人物xも,(生みの)母というのは唯一に定まるからである.  もちろん,述語記号を用いて,    MOTHER(x, y): y is the mother of x のように表現することも可能であるが,この場合,y が x から一意に定まるオブジェクトであることは,コンピュータにはわからない.(もちろん,応用上,それで良いなら問題はない.)

表現の技法(5/9) ∀と→の組合せ 「P は Q である」 という一般的な叙述は,(∀x)( P(x) → Q(x) ) のパターン使う. (1) 花は美しい. Flower is beautiful. (∀x)( FLOWER(x) → BEAUTIFUL(x) ) (2) 偶数は2で割り切れる. Every even number is divided by 2. (∀x)( EVEN(x) → DIVIDES(s(s(0)), x) )  全称記号や存在記号自体の意味は単純なものだが,他の論理的記述とからんでくると表現がむずかしくなってくる.このスライドでは,全称記号の典型的な使用パターンを学んでおこう.  PとQが普通名詞や形容詞など,述語記号で表現できるものであるとする.このとき,    「PはQである」 というタイプの叙述が知識として良く使われる.そのような知識の表現は     (∀x)( P(x) → Q(x) ) とするのが一般的である.すなわち,直訳すると,    「任意のxについて,xがPという性質をもつならば,xはQという性質をもつ」 というように表現する.全称記号∀と含意記号→の組合せは相性が良いので,よく組み合わせて用いられる.

表現の技法(6/9) ∃と∧の組合せ 「 a +普通名詞」 は,∃ と ∧ の組合せを使う.   ジャックはある女性を愛している. Jack loves a woman. (∃w)(WOMAN(w) ∧LOVES(Jack, w))  存在記号は,不定のあるオブジェクトを指し示しているので,英語では     「不定冠詞(a, an)+普通名詞」 あるいは,さらに,普通名詞が形容詞で修飾されて    「不定冠詞(a, an)+形容詞+普通名詞」 で表されることが多い.そのときは,変数xを(∃x)のようにして導入し,xの満たすべき性質(形容詞や普通名詞を記号化した述語)をANDで結合すればよい.このように,存在記号∃はAND記号∧と相性が良い.

「任意のx に対し,あるy が存在し,P(x,y) が成り立つ」 全称記号と存在記号の出現順序が意味をもつ 任意のx に対し,あるy が存在し,P(x,y) が成り立つ P(x,y) a b c T F y x  一般に,全称記号と存在記号の出現順序は,きわめて重要である.順序によって意味が異なってくるのである.  このスライドの例の場合,(∀x)(∃y)P(x,y) という論理式は, 「任意のx に対し,あるy が存在し,P(x,y) が成り立つ」 と読むのだが,ここでは, ∀xが∃yの外側(左側)にあることが重要である.  トランプ手品のような状況を想定するとわかりやすい.まず最初に任意のカードxを誰かに選んでもらう.そうすると,x として何が来ようと,その後,私たち(手品師)はその x に依存してカード y をその都度うまく選ぶことができて,命題 P(x,y) を真として,客を驚かせることができるのである.  たとえば,解釈の定義域DとしてD={a,b,c}を考え,述語Pをこのスライドの表によって解釈しよう.すると,どのxを最初に選んでも,それに依存して,P(x,y)=T となるようにyを選ぶことができるので,論理式(∀x)(∃y)P(x,y)は真である.

「あるy が存在し,任意のx に対し,P(x,y) が成り立つ」 全称記号と存在記号の出現順序が意味をもつ あるy が存在し,任意のx に対し,P(x,y) が成り立つ P(x,y) a b c T F y x  こんどは,(∀x)と(∃y)の順序を入れ換えた論理式(∃y)(∀x)P(x,y) を考えてみる.これは, 「あるy が存在し,任意のx に対し,P(x,y) が成り立つ」 と読むのだが,ここでは, ∃yが∀xの外側(左側)にあることが重要である.さきほどの手品からの類推で言えば,私たちはまず事前にカード y を1つ適切に選んでおく.それ以降は y は固定され,変えることはできない.そうすると,その後は, 誰かに自由に選ばせたカード x として何が来ようと,すべての x に対して,命題 P(x,y) が真となるのである.  たとえば,解釈の定義域DとしてD={a,b,c}を考え,述語Pをこのスライドの表によって解釈しよう.すると,y=bに選んでおけば,その後,どのxに対しても,P(x,y)=T となるので,この論理式は真である.

表現の技法(9/9) 技法の組合せ (1) すべての男性はある女性を愛している. Every man loves a woman. (∀m)( MAN(m) → (∃w)(WOMAN(w) ∧LOVES(m, w)) 各男性(m)ごとに,愛している女性(w)が異なる (2) すべての男性が愛する女性がいる. There exists a woman every man loves. (∃w) (WOMAN(w) ∧ (∀m)( MAN(m) → LOVES(m, w)) )  これまで学んだ技法を組み合わせた表現を見ておこう.  (1)の例では,∀mが∃wの外側(左側)にある.まず,任意の男性mを考えると,そのmに依存して女性wが存在して,mはwを愛しているのである.したがって,m=Jackのときはw=Elizabethかもしれないが,mが別の男性のときはwは他の女性かもしれない.  (2)の例のように, ∃wが∀mの外側(左側)になると,まず,ある女性wが存在することが宣言される.すると,すべての男性mはその女性wを愛しているというのである.すなわち,全男性は特定の1名の女性を愛していることになる.たとえば,敬虔なキリスト教の世界だと,そのwという女性はマリア様かもしれない.あるいは,大学の小さな研究室内で女性が1名しかいない集団を定義域Dとすれば,そのようなことがあるかもしれない. 全男性(m)が,特定の1人の女性(w)を愛している

節集合への変換

節形式への変換の概要 一階述語論理の論理式 等価 冠頭標準形 連言標準形 等価ではないが,充足可能性は保存 スコーレム標準形 節集合 1.同値と含意を除去する 2.否定を原子論理式の直前に移す 3.変数名を付け替える 4.冠頭標準形にする 冠頭標準形 連言標準形 5.連言標準形にする 等価ではないが,充足可能性は保存 スコーレム標準形  命題論理のところで,すべての命題論理式を連言標準形(CNF)に変換し,それを節の集合として表現し,融合原理に基づく推論規則によって,論理的帰結となる節を導出する方法を学んだ.一階述語論理でも同様なことが可能である.今回は,その準備として,任意の一階述語論理式を節集合に変換する方法を学ぼう.  ただし,その変換は一気にはできない.スライドに示す幾つかのステップをふむ必要がある. 6.スコーレム標準形にする 節集合 7.節集合にする

冠頭標準形への変換(1) 冠頭標準形 論理式は次の形をしているとき冠頭標準形であるという. ただし,各 は, か であり,  論理式は次の形をしているとき冠頭標準形であるという. ただし,各        は, か   であり, M は限量子を含まない論理式である.  冠頭標準形とは, (∀x)や(∃y)のような限量子が,すべて論理式の最も外側(=左端,頭部)に集まっている形のことである.限量子が集まった部分を前置部,それ以外を母式という.任意の論理式は,それと等価な冠頭標準形に変換できる. 例

休憩

冠頭標準形への変換(2) 1.同値と含意を除去する 2.否定を原子の直前まで移す  この2つのステップは,命題論理のときにも学んだものである.ただし,一階述語論理の場合には,限量子を扱う最後の2つの規則が追加される.この2ステップが終了すれば,論理式からすべての同値記号と含意記号が削除され,否定記号は原子式の直前まで移動されていることになる.

冠頭標準形への変換(3) 3.変数名を付け替える 各限量子に対応する変数が他の限量子に対応する 変数と同じ名前にならないように必要に応じて付 例 ステップ4  つぎの第4ステップで限量子を外側に移動する処理を行うのだが,その準備として,必要に応じて限量子の名前を付け替えておく.基本的に,すべての限量子の名前を付け替えて問題がない.ただし,その必要がない場合もあるので,つぎのスライドで示す.

冠頭標準形への変換(4) NOTE M(x): x is a man. W(x): x is a woman. NOTE 下記のケースは付け替えなくても良い  最初の2つの式は,変数名を付け替える必要性を示している.M(x)を「xは男性である」,W(x)を「xは女性である」と解釈すると,各論理式の意味はつぎにようになる.  (∀x)M(x)∨(∀x)W(x):「全員が男性または全員が女性である」(たとえば,混浴でない風呂場)  (∀x)(M(x)∨ W(x)):「全員が男性または女性である」(中性がいない普通の状況)  (∃x)M(x)∧(∃x)W(x):「男性も女性も少なくとも1名存在する」(男女混合ダブルス)  (∃x)(M(x)∧ W(x)):「男性かつ女性であるオブジェクトが存在する」(両性か!)  (∀x)M(x) ∧ (∀x)W(x)= (∀x)(M(x) ∧ W(x)) :「全員が男性かつ女性である」(全員が両性生物の世界)  (∃x)M(x)∨ (∃x)W(x) =(∃x)(M(x)∨ W(x)) :「男性または女性が存在する」(普通の人が1人でもいる世界)

冠頭標準形への変換(5) 4.冠頭標準形にする 限量子を外側(左側)に移動する  このスライドの3,4番目のケースは2つの限量子が同じでもよいが,それ以外の場合は,限量子を変数名を必要に応じて付け替えながら,それぞれ外側へ移動する.

冠頭標準形への変換(5) 例  冠頭標準形に変換する例題.

連言標準形への変換(1) リテラル 原子式 はリテラルである. 正リテラル 例 原子式 はリテラルである. 負リテラル 節 原子式 はリテラルである. 正リテラル 例   原子式 はリテラルである. 負リテラル 節 リテラルの選言(orで結合したもの) 例 連言標準形  1個の原子式,または,その否定をリテラルという.とくに,前者を正リテラル,後者を負リテラルという.  リテラルの宣言(orで結合したもの)を節という.  節の連言(andで結合したもの)を連言標準形という.  したがって,連言標準形では最も外側では and 記号が現れて節を結合しており,各節の内部では or 記号がリテラルを結合し,リテラルの内部では not 記号が現れるというように,and, or, not が整然とした入れ子構造の中に配置されている. 節の連言(andで結合したもの) 例

連言標準形への変換(2) 5.連言標準形にする 冠頭標準形 M を連言標準形にする 分配則を使って∨を入れ子の内側へ移動していき,リテラル同士を直接接合するようにする  すでに得られている冠頭標準形の母式Mを,分配則を使って,連言標準形にすることができる.

スコーレム標準形への変換(1) スコーレム標準形 6.スコーレム標準形にする 冠頭標準形 M が連言標準形 存在記号をすべて除去する ・等価性は失われる ・充足可能性は変わらない スコーレム標準形  ここまでで,論理式は冠頭標準形になっていて,その母式は連言標準形になっている.ここで,以下のスライドで述べる方法で,すべての存在記号∃を除去した論理式をスコーレム標準形という.  重要な点は,この変形によって論理式の等価性は失われるということである.なぜなら, ∃を除去するのと引き替えに,その論理式に今まで含まれていなかった新しい個体記号(定数)や新しい関数記号を導入することになるからである.  しかし,変換前の論理式と変換後の論理式では,充足可能性は変わらない.一方が充足可能なら,他方も充足可能である.また,一方が充足不能なら,他方も充足不能である.論理式が事前知識の論理的帰結かどうかは,命題論理のときと同様に,等価性の判定ではなく,充足可能性の判定に帰着されるので,それを目的とする場合には,この変形が有用なのである. スコーレム標準形への変換手順:  最も左にある存在記号に着目し,以下の処理(つぎの2つのスライド)を存在記号がなくなるまで繰り返す

スコーレム標準形への変換(2) のとき 1.M に現れない新しい定数 a を任意に選び,M中のすべての を a で置き換える. a をスコーレム定数という. 2. を前置部から除去する 例  スコーレム標準形への変換は,論理式の中の存在記号∃のうち,最も左にあるものに着目し,それを除去する.その存在記号のさらに左に全称記号∀があるかないかで,2つのケースがある.  このスライドは,除去する (∃x1)のさらに左に全称記号∀がない場合,スコーレム定数というこれまで論理式に含まれていなかった新しい定数(たとえば,a)を導入し,母式の中のx1をそれで置き換えることを示している.

スコーレム標準形への変換(3) のとき 1.M に現れない新しい関数記号 f を任意に選び,M中のすべての を       で置き換える.f をスコーレム関数という. 2. を前置部から除去する 例  除去する (∃xk)のさらに左に全称記号∀がある場合,スコーレム関数というこれまで論理式に含まれていなかった新しい関数記号(たとえば,f )を導入し,その引数に (∃xk)の左側に出現している各∀の右にあるすべての変数を書き込んだ項で母式の中のxkを置き換える.

節集合への変換 7.節集合にする スコーレム標準形 M が連言標準形 Mに含まれている節を集める 節集合 例  ここまで来れば,母式の中のすべての節を集めた集合が節集合となる.  節集合に含まれるそれぞれの節の中の変数 x は,暗黙裏に,(∀x)で限量されていることに注意しよう.すなわち,「 任意の x について...」と読むわけである.