述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能

Slides:



Advertisements
Similar presentations
プログラミング言語論 第3回 BNF 記法について(演習付き) 篠埜 功. 構文の記述 プログラミング言語の構文はどのように定式化できるか? 例1 : for ループの中に for ループが書ける。 for (i=0; i
Advertisements

2.5 プログラムの構成要素 (1)文字セット ① ASCII ( American Standard Code for Interchange ) JIS コードと同じ ② EBCDIC ( Extended Binary Coded Decimal for Information Code ) 1.
一階述語論理 (first-order predicate logic) 一階述語論理入門 構文論(論理式の文 法) 意味論(論理式の解 釈) 認知システム論 知識と推論(4) 知識と論理でを組み合わせて問題を解決する.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
人工知能特論2011 No.4 東京工科大学大学院 担当教員:亀田弘之.
人工知能特論2007 No.4 東京工科大学大学院 担当教員:亀田弘之.
白井 良明 立命館大学情報理工学部 知能情報学科
計算の理論 II 帰納的関数(つづき) 月曜4校時 大月美佳.
節集合 (set of clauses) 認知システム論 知識と推論(5) 一階述語論理による知識表現の技法 節集合への変換
データ構造と アルゴリズム 理工学部 情報システム工学科 新田直也.
充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.
計算の理論 II NP完全 月曜4校時 大月美佳.
演習3 最終発表 情報科学科4年 山崎孝裕.
プログラミング言語論 第4回 式の構文、式の評価
プログラミング言語論 第1回 導入 情報工学科 篠埜 功.
人工知能特論2011 資料No.6 東京工科大学大学院 担当教員 亀田弘之.
立命館大学 情報理工学部 知能情報学科 谷口忠大
条件式 (Conditional Expressions)
数理論理学 第1回 茨城大学工学部情報工学科 佐々木 稔.
9.NP完全問題とNP困難問題.
データ構造と アルゴリズム 知能情報学部 新田直也.
プログラミング言語論 第1回 導入 情報工学科 篠埜 功.
エージェントアプローチ 人工知能 7章・8章 B4 片渕 08/07/18.
コンパイラ 2012年10月22日
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
数理論理学 第11回 茨城大学工学部情報工学科 佐々木 稔.
コンパイラ 2011年10月24日
命題論理 (Propositional Logic)
寄せられた質問: 演習問題について この講義の範囲に含まれる適切な演習問題が載っている参考書がありますか? できれば解答や解説が付いているものがあると良いのですが… 第3回の授業の中で、演習問題に取り組む方法を説明します.
不完全な知識 不完全な知識に基づく問題解決 フレーム問題 制約条件記述問題 非単調推論 極小限定 常識の定式化 並列極小限定.
プログラムの制御構造 選択・繰り返し.
2. 論理ゲート と ブール代数 五島 正裕.
プログラミング言語論 第3回 BNF記法について(演習付き)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
述語論理と∀(全称)∃(存在) 3回の講義の概観: 命題論理 (真理値) (公理と推論規則) 述語論理 (モデルと解釈)
暗黙的に型付けされる構造体の Java言語への導入
数理論理学 第3回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング入門2 第11回 情報工学科 篠埜 功.
Prolog入門 ーIT中級者用ー.
 型推論1(単相型) 2007.
述語論理.
論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則
計算機科学概論(応用編) 数理論理学を用いた自動証明
論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog
9.通信路符号化手法1 (誤り検出と誤り訂正の原理)
知能情報システム特論 Introduction
数理論理学 第12回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第9回 情報工学科 木村昌臣 篠埜 功.
 型推論3(MLの多相型).
第6章-2 計算のモデル オートマトン Turing 機械 計算可能性 1.
言語表現と 視覚表現の比較 関西大学社会学部 雨宮俊彦.
上のURLはシラバスに掲載されている (念のために次ページに拡大表示します)
Prolog入門 ーIT中級者用ー.
文法と言語 ー文脈自由文法とLR構文解析ー
第14回 前半:ラムダ計算(演習付) 後半:小テスト
第7回  命題論理.
東京工科大学 コンピュータサイエンス学部 亀田弘之
東京工科大学 コンピュータサイエンス学部 亀田弘之
数理論理学 第9回 茨城大学工学部情報工学科 佐々木 稔.
プログラミング言語論 第10回 情報工学科 篠埜 功.
4.プッシュダウンオートマトンと 文脈自由文法の等価性
第6回放送授業.
モデルの微分による非線形モデルの解釈 明治大学 理工学部 応用化学科 データ化学工学研究室 金子 弘昌.
香川大学工学部 富永浩之 情報数学1 第5-2章 命題論理式の 同値変形とカルノー表 香川大学工学部 富永浩之
オブジェクト指向言語論 第二回 知能情報学部 新田直也.
コンパイラ 2012年10月11日
PROGRAMMING IN HASKELL
数理論理学 最終回 茨城大学工学部情報工学科 佐々木 稔.
立命館大学 情報理工学部 知能情報学科 谷口忠大
オブジェクト指向言語論 第六回 知能情報学部 新田直也.
Presentation transcript:

述語論理式の構文と意味 一階述語論理式の構文 一階述語論理式の意味 述語,限量記号 自然言語文の述語論理式表現 解釈 妥当,充足不能 閉式の充足不能性

述語論理 述語(predicate)の導入 「太郎は人間である」 「花子は人間である」 命題論理による表現 述語論理による表現 述語 「太郎は人間である」  「花子は人間である」 命題論理による表現 述語論理による表現 述語 「・・・人間である」という共通する情報が欠落してしまう

述語論理 限量記号(quantifier)の導入 は である: すべての  は  である:  ある  は  である: 全称記号 存在記号

一階述語論理の構文 語彙 個体定数(constant): 個体変数(variable): 関数記号(function symbol): 述語記号(predicate symbol): 論理記号(connective): 限量記号(quantifier): 補助記号(punctuation symbol):

一階述語論理の構文 項(term)の帰納的定義 (1)個体定数は項である. (2)個体変数は項である. (3) が 引数の関数記号, が項 (3)  が  引数の関数記号,     が項   ⇒        は項である. (4)項とは(1),(2),(3)を有限回繰り返し適用して得られる記号列のみである.

一階述語論理の構文 整式(wff)の帰納的定義 (1) が 引数の述語記号, が項 ⇒ は整式(素式)である. (2) が整式 (1)  が  引数の述語記号,     が項   ⇒        は整式(素式)である. (2)    が整式   ⇒                   は整式である. (3)  が整式,  が個体変数   ⇒       は整式である. (4)整式とは(1),(2),(3)を有限回繰り返し適用して得られる記号列のみである.

限量記号の作用 作用域(scope): の (ただし ) 束縛変数(bound variable): の に現れる 自由変数(free variable): 束縛変数以外の変数 束縛変数 束縛変数 自由変数

限量記号の作用 束縛関係: の と部分式 の自由変数 は に束縛されるという. 束縛関係:    の  と部分式  の自由変数  は  に束縛されるという. 閉式(closed formula): すべての変数が束縛されている整式で,文(sentence)ともいう. 自由変数 自由変数

自然言語文→述語論理式表現 翻訳の基本パターン すべてのものが である.(Everything is p.) ⇒      ⇒   なものが存在する.(Something is p.)   ⇒ すべての  は  である.(Every p is q.) ある  は  である.(Some p is q.)

自然言語文→述語論理式表現 なぜ 「ある p は q である」 を 「 」と表現すべきなのか? 「ある p は q である」 否定 否定

表現の例 ① 試験が難しい科目の受験者は皆喜ばない. ② 試験が難しくなければ喜ぶ受験者がいる. ③ 数学の受験者しか喜ばない. ① ② ③ ① 試験が難しい科目の受験者は皆喜ばない. ② 試験が難しくなければ喜ぶ受験者がいる. ③ 数学の受験者しか喜ばない. ① ② ③ : x は試験が難しい. : x は y の受験者である. : x は喜ぶ. : 数学.

一階述語論理式の意味 解釈(interpretation): 変数割り当て: 領域(domain): D 割り当て: (1)個体定数 c : (2)関数記号 f : (3)述語記号 p : 変数割り当て: 個体変数 x に対して : x に     を割り当て,x 以外には             による割り当てをする変数割り当て.

一階述語論理式の意味      による意味評価

述語論理式を解釈してみよう

充足可能性 :論理式 :解釈 :変数割り当て は を充足する( ). を充足する が存在する(しない). は充足可能(不能)である.   :論理式   :解釈   :変数割り当て              は  を充足する(     ).   を充足する が存在する(しない).        は充足可能(不能)である. 任意の  について        は  を充足する(    ).   が閉式  (またはその集合  )を充足す  るとき,  を  (または  )のモデルという.

妥当性 任意の解釈と任意の変数割り当てが論理式 を充足するとき, は妥当であるという( ). は妥当である. は充足不能である. 任意の解釈と任意の変数割り当てが論理式  を充足するとき, は妥当であるという(   ).  は妥当である.     は充足不能である.      任意の     について       任意の    ,    について       任意の     について 閉式

論理的帰結 を充足する任意の解釈と任意の変数割り当てが必ず を充足するとき, は の論理的帰結であるという( ). :論理式の集合 :論理式   :論理式の集合   :論理式    を充足する任意の解釈と任意の変数割り当てが必ず  を充足するとき,  は  の論理的帰結であるという(     ). 閉式 は充足不能である.

閉式の充足不能性 閉式 の充足不能性を考える. 命題論理式 が恒偽な命題論理式であれば 任意の解釈 で 一般には決定できない 閉式      の充足不能性を考える. 一般には決定できない ある   がFであれば決定できる 命題論理式 が恒偽な命題論理式であれば 任意の解釈   で

閉式の充足不能性 恒偽 恒偽 標準的解釈

まとめると… 一階述語論理式の充足不能性           閉式の充足不能性       の充足不能性 充足不能であれば決定可能            標準的な解釈の存在