述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)

Slides:



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

プログラミング言語論 第3回 BNF 記法について(演習付き) 篠埜 功. 構文の記述 プログラミング言語の構文はどのように定式化できるか? 例1 : for ループの中に for ループが書ける。 for (i=0; i
論理回路 第 11 回
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
0章 数学基礎.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
第3回 論理式と論理代数 本講義のホームページ:
第1章 数と式 第4節 集合と命題  8  集合 (第3回).
ファジィ論理と ファジィ構造モデリング 北海道工業大学 情報デザイン学科 三田村 保.
節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換
アルゴリズムとデータ構造1 2007年6月12日
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
演習3 最終発表 情報科学科4年 山崎孝裕.
プログラミング言語論 第4回 式の構文、式の評価
論理式の表現を数学的に取り扱いやすくするために代数学の助けを借りる.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
立命館大学 情報理工学部 知能情報学科 谷口忠大
人工知能特論2011 No.3 東京工科大学大学院 担当教員:亀田弘之.
情報教育論 第9回 仮定文の仕組み 政策・メディア研究科 岡田 健.
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
9.NP完全問題とNP困難問題.
最尤推定によるロジスティック回帰 対数尤度関数の最大化.
「情報数学06前再」の注意事項 このページの内容は  「情報数学06前再」(3単位)を履修している諸君には上田先生からの連絡が届きます。 「06前再」の受講者は,情報理工学科の「情報数学」
需要の価格弾力性 価格の変化率と需要の変化率の比.
ターム分布の確率モデル Zipfの法則:使用頻度の大きな語は語彙数が少なく,使用頻度の小さな語は語彙数が多い
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
4. 組み合わせ回路の構成法 五島 正裕.
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
第4章 組合せ論理回路 (4) Quine McCluskeyの方法.
ディジタル回路 3. 組み合わせ回路 五島 正裕 2018/11/28.
2. 論理ゲート と ブール代数 五島 正裕.
プログラミング言語論プログラミング言語論 プログラムの意味論 水野嘉明
プログラミング言語論 第3回 BNF記法について(演習付き)
計算の理論 II NP完全 月曜5校時 大月美佳 平成17年1月17日 佐賀大学理工学部知能情報システム学科.
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
形式言語の理論 5. 文脈依存言語.
ディジタル回路 2. ブール代数 と 論理ゲート 五島 正裕.
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
 型推論1(単相型) 2007.
述語論理.
「情報数学06前再」の注意事項 このページの内容は 
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
9.通信路符号化手法1 (誤り検出と誤り訂正の原理)
知能情報システム特論 Introduction
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
2007年 4 月~7 月( 合計12回予定) 講義資料: 上田 和紀 原著 後藤 滋樹 三訂
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
 型推論3(MLの多相型).
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
第14回 前半:ラムダ計算(演習付) 後半:小テスト
第7回  命題論理.
論理回路 第5回
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第10回 情報工学科 篠埜 功.
述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能
再履修の諸君への連絡事項 このページの内容は 
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
4.プッシュダウンオートマトンと 文脈自由文法の等価性
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
情報処理Ⅱ 2005年11月25日(金).
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
練習問題.
練習問題.
Presentation transcript:

述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈) 1 2 3 意味論 semantics syntax 構文論

preview 述語論理は命題論理よりも複雑 例題: 次の文は真か偽か? 「すべての自然数 x に対して x < y を満たすような自然数 y が存在する」   (小野先生の例題) 解釈(その一) すべての x に対して「 x < y を満たすような y が存在する」 :∀x ∃y (x < y) 解釈(その二) 「すべての x に対して x < y を満たす」ような y が存在する :∃y ∀x (x < y) 曖昧

述語と対象変数 P : D×D  T, 2変数(引数)の述語 復習 命題とは真理値(真偽)が確定している文のこと 真偽のいずれかの値 { t, f } をとる:命題変数 対象変数を含む文の真理値は確定しない 例: x ≦ 200 y は素数である このような文を扱うために 命題関数 P を考える P : D  T, ここに T = { t, f } 例: 対象領域 D として自然数の集合を考える P : D×D  T, 2変数(引数)の述語 対象変数 individual variable, object variable 命題関数 propositional function

述語 predicate ↑ 正確な記法を次に述べる。∀と∃が多重になるときに注意 述語: 命題関数の具体的な表現 例: Le, Prime Le (x, 200) : (x ≦ 200 ), 2変数(引数) Prime (y) : 「 y は素数である」 対象領域 D の要素を対象 object, individual という 対象領域 D の上を動く変数を対象変数、D の定数を対象定数 object (individual) constant という 全称記号∀, と存在記号∃ ∀x P(x): すべての x∈D に対して P(x) が真になる ∃y Q(y): ある y ∈D が存在して Q(y) が真になる 述語記号 ↑ 正確な記法を次に述べる。∀と∃が多重になるときに注意

述語論理の項 term 今までに登場したもの: 対象変数、対象定数 今までに登場したもの: 対象変数、対象定数 さらに必要なもの: 対象領域の上の関数記号 関数記号の例: 自然数の上の +, × 項 term の定義: 個々の対象定数、対象変数は項である f が n 変数(引数)の関数記号で, t1, t2, …, tn が項であるならば f (t1, t2,…, tn) は項である 項の例: 200, x, y, (3+x), 6×(x+y). +(3,x), ×(6, +(x, y)) とも書く

論理式 formula, wff 述語記号: 述語を表す記号 述語記号: 述語を表す記号 P が n 変数(引数)の述語記号で t1, t2, …, tn が項ならば 、P(t1, t2, …, tn) は論理式である A, B が論理式ならば、 A∧B, A∨B, A⇒B, ¬Aは、いずれも論理式である A が論理式で x が対象変数ならば 、 (∀x A), (∃x A) は論理式である 注:「1」の形の論理式を原子(atomic)論理式 という 復習:⇔は省略してよい 例: ∀x(∀y(∃q(∃r(x=q×y+r)))), = は述語記号

∀, ∃ quantifier 限定記号, 量化記号, 限量子 「すべての x に対して R(x, y) を満たす y が存在する」 という文は曖昧である ∀x ∃y (x < y) すべての自然数 x に対して,x よりも大きな 自然数 y (例えば x+1 )が存在する (真) ∃y ∀x (x < y) ある自然数 y が存在して,y は如何なる (すべての)自然数 x よりも大きい (偽) 前出

自由変数と束縛変数 free and bound variables ∀x ∃y (x < y) の変数 x, y は、変数と呼ばれているが、代入の対象にならない ∀z ∃y (z < y) と書いても意味が変わらない 変数には2種類ある。自由変数と束縛変数 ここで注意するべき事は、同じ変数が自由であり、同時に束縛されることがある 例: ∃y (x = y+y )∧ ∃z ( y = z+z+1 ) x は偶数である y は奇数である 自由変数と束縛変数を出現 occurrenceという単位で区別しなければならない 

出現 occurrence A が原子論理式であるとき、A に含まれる変数 x の出現は、すべて自由な出現である A が B∧C, B∨C, B⇒C, ¬B のいずれかであるとする。もし x が B または C における自由な出現であるならば、その x は A において自由である。もし x が B または C における束縛された出現であるならば、その x は A において束縛されている A が (∀z B) または (∃z B) であるとする。もし z が x であるときは、Aにおける x の出現は束縛されている。 z が x と異なる場合には、もし x が B における自由な出現であるならば、その x の出現は A において自由である。もし x が B における束縛された出現であるならば、その x の出現は A において束縛されている

自由変数と束縛変数(例) 例: ∃y (x = y+y )∧ ∃z ( y = z+z+1 ) 論理式が自由変数を一つも含まない時 閉論理式 closed formula という 論理式 A に含まれる自由変数 x に項 t を代入して得られる論理式を A[t/x] と表す 代入をめぐる珍現象: (小野先生の例題) ∃z(x=y×z)  : x は y の倍数である ∃z(x=100×z) : x は 100 の倍数である ∃z(x=z×z)  : x は平方数である これを避けるために自由変数と束縛変数の記号の種類を分ける流儀の教科書もある

代入の方法 A は ∀zB または ∃zB の形の論理式とする A[t/x]は z が x のとき A[t/x] は A 自身(束縛変数に代入不可) z が x とは異なる変数のとき、 t に z が出現しなければ、 A[t/x] は ∀zA[t/x] または ∃zA[t/x] t に z が出現する場合は、 A[t/x] は ∀w((A[w/z])[t/x]) または ∃w((A[w/z])[t/x] ) ただし w は A にも t にも現れない新しい対象変数 i.e. 項 t に変数 w が現れることがない

論理式の意味 述語論理の論理式の意味を考えるには、対象領域domain を定める必要がある (解釈 interpretation, モデル model, 構造 structure) 空でない集合 D を定める 対象定数に D の要素(元)を対応づける 対象変数は D の上を動く 関数記号に D の上の関数を対応づける 述語記号に D の上の述語を対応づける ※ 単なる記号 に 具体的な要素、関数、述語 を対応 ※ ただし述語記号 = (等号)の解釈は通常の等号とする

解釈 ⊨ 閉論理式 M ⊨ A 解釈 M において論理式 A が真 M ⊭ A 解釈 M において論理式 A が偽 ⊭⊨ M ⊨ A 解釈 M において論理式 A が真 M ⊭ A 解釈 M において論理式 A が偽 A が原子論理式のとき M ⊨ P(t1, t2, …, tn) となるのは、Pの解釈が項 t1, t2, …, tn の解釈において真になる場合である. M ⊨ A∧B となるのは (M ⊨ A かつ M ⊨ B ), M ⊨ A∨B となるのは(M ⊨ A または M ⊨ B), M ⊨ A⇒B となるのは (M ⊨ A ならば M ⊨ B), M ⊨ ¬A となるのは M ⊭ A の時である . ⊭⊨ : MSゴシック(UTF) M: Lucida Calligraph

(続) 解釈 ⊨ 閉論理式 M ⊨ ∀x A となるのは、すべての D の要素 u に対して M ⊨ A[u/x] となるとき, (続) 解釈 ⊨ 閉論理式 ⊭⊨ M ⊨ ∀x A となるのは、すべての D の要素 u に対して M ⊨ A[u/x] となるとき, M ⊨ ∃x A となるのは、D のある要素 u が存在して M ⊨ A[u/x] となるときである. 論理式 B に対して、B に含まれる自由変数 が x1, x2, …, xm であるとき、 ∀x1∀x2…∀xm Bを B の閉包 universal closureという. BC と書く M ⊨ B となるのは M ⊨ BC となるときである. ⊭⊨ : MSゴシック(UTF) M: Lucida Calligraph

恒真な(valid)論理式 いかなる解釈(モデル)に対しても真になる論理式を恒真な valid 論理式という 「述語論理におけるトートロジー」ということもある どのような解釈をしても真になるということは、個別の対象要素、関数記号、述語記号の解釈に依存しないという意味である すなわち論理式の形(構造)により、恒真であるか否かが定まる

恒真な論理式の例(その一) A は x を自由変数として含まない ∀x A ⇔ A, ∃x A ⇔ A ∀x B ⇔ ∀y(B[y/x]), ∃x B ⇔ ∃y (B[y/x]) ここに y は B に含まれていない新しい変数 A ∧ ∀x B ⇔ ∀x (A∧B), A ∨ ∃x B ⇔ ∃x (A∨B) A ∨ ∀x B ⇔ ∀x (A∨B), A ∧ ∃x B ⇔ ∃x (A∧B) ∀x B ∧ ∀x C ⇔ ∀x (B∧C), ∃x B ∨ ∃x C ⇔ ∃x (B∨C) (∀x B ∨ ∀x C) ⇒ ∀x (B∨C), ∃x(B ∧ C) ⇒ (∃x B∧∃x C)

恒真な論理式の例(その二) ∀x∀y B ⇔ ∀y∀x B , ∃x∃y B ⇔ ∃y∃x B ∃x∀y B ⇒ ∀y∃x B ∀x B ⇒ ∃x B ¬∀x B ⇔ ∃x¬B, ¬∃x B ⇔ ∀x¬B (A ⇒∀x B) ⇔ ∀x(A ⇒ B), (A ⇒∃x B) ⇔ ∃x(A ⇒ B) (∀x B ⇒ A) ⇔ ∃x(B ⇒ A), (∃x B ⇒ A) ⇔ ∀x(B ⇒ A) ∃x(B ⇒ C) ⇔ (∀x B ⇒ ∃x C) ∀x(B ⇒ C) ⇒ (∀x B ⇒ ∀x C) ∀x(B ⇒ C) ⇒ (∃x B ⇒ ∃x C) (関連の話題が前出) ド・モルガンの法則

恒真な論理式の説明 (∃x B ⇒ A) ⇔ ∀x(B ⇒ A) この論理式に含まれる自由変数が y1, …, ym のとき、任意の解釈 M について次をいえばよい M ⊨∀y1…∀ym{(∃x B ⇒ A) ⇔ ∀x(B ⇒ A)} 上は閉論理式であるから次をいう(解釈 4, 6) すべての u1, …,um ∈ D に対して M ⊨(∃x B ⇒ A)[u1/y1,…,um/ym] ⇔ M ⊨ ∀x(B ⇒ A) [u1/y1,…,um/ym] 以下では、既に項の代入が済んでいると仮定

恒真な論理式の説明(2) M ⊨ (∃x B ⇒ A) ⇔ M ⊨ ∀x(B ⇒ A) M ⊨(∃x B ⇒ A) であると仮定する. これは解釈4と7から「(ある v∈D が存在して M ⊨ B[v/x]) ならば(M ⊨ A)である 」 ということになる 上は「(M ⊨ B[v/x] を満たすような v∈D は存在しない)または(M ⊨ A)である 」となる さらに「(すべての v∈D に対して M ⊭ B[v/x] )または(M ⊨ A)である 」となる 論理式 A は x を自由変数として含まない 「(すべての v∈D に対して (M ⊭ B[v/x] またはM ⊨ A[v/x])である 」 半分終り

恒真な論理式の説明(3) M ⊨ (∃x B ⇒ A) ⇔ M ⊨ ∀x(B ⇒ A) M ⊨∀x(B ⇒ A) であると仮定する. 解釈6と4から「すべての v∈D に対して(M ⊨ B[v/x] ならば M ⊨ A[v/x])である 」 になる 論理式 A は x を自由変数として含まない「すべての v∈D に対して(M ⊭ B[v/x] または M ⊨ A )」 「(すべての v∈D に対してM ⊭ B[v/x])または (M ⊨ A)である )」,さらに「(M ⊨ B[v/x] を満たすv∈D は存在しない) または(M ⊨ A)である 」 「(M ⊨ B[v/x] を満たすv∈D が存在する) ならば (M ⊨ A)である 」 終

充足可能な論理式 ある解釈(モデル)に対して真になる論理式を充足可能な satisfiable 論理式という 充足可能でない論理式を充足不可能 unsatisfiable という 論理式 A が充足不可能であることは、¬A が恒真であることの必要十分条件である

冠頭標準形 prenex normal form 全称記号∀と存在記号∃が、他の論理記号の外側にあるとき、冠頭論理式という QxQyQz…A, Qは∀あるいは∃記号 A は全称記号も存在記号も含まない論理式 論理式 A と同値な冠頭論理式が存在する これを冠頭標準形という (小野先生の説明) 恒真な論理式の 3, 4, 10, 11, 12 を使って同値変形する。ただし A が自由変数 x を含むときは、まず 2. により x を新しい変数で置き換えておく

冠頭標準形への同値変形 ¬∃yP(x,y)∧∀y{∃zQ(x,y,z)⇒R(x,y)} ¬∃yP(x,y)∧∀w{∃zQ(x,w,z)⇒R(x,w)} ∀y¬P(x,y)∧∀w{∃zQ(x,w,z)⇒R(x,w)} ∀y∀w{¬P(x,y)∧(∃zQ(x,w,z)⇒R(x,w))} ∀y∀w{¬P(x,y)∧∀z(Q(x,w,z)⇒R(x,w))} ∀y∀w∀z{¬P(x,y)∧(Q(x,w,z)⇒R(x,w))} さらに ∀y∀w∀z{¬P(x,y)∧(¬Q(x,w,z)∨R(x,w))} ∀y∀w∀z{(¬P(x,y)∧¬Q(x,w,z))       ∨( ¬P(x,y)∧R(x,w))} 訂正: 廣瀬先生のp.24, ∃zは∀zです 分配法則

冠頭標準形 (廣瀬先生の説明) 与えられた述語の中の別の変数が同じ変数の記号で表されているとき、すべて異なる変数に書き換える (廣瀬先生の説明) 与えられた述語の中の別の変数が同じ変数の記号で表されているとき、すべて異なる変数に書き換える 例: ∀x P(x,y)∨∃y Q(y,z)は∀x P(x,y)∨∃w Q(w,z) ∃x P(x)∧∀x Q(x, y)は∃x P(x)∧∀z Q(z, y) ド・モルガンの法則を用いて否定記号¬を内側に移動する(10) 全称記号∀と存在記号∃を外側に移動する (3, 4, 11, 12) さらに、冠頭標準形と論理和標準形、冠頭標準形と論理積標準形を組合せることができる