論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則

Slides:



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

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

論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論 推論規則 推論の妥当性:論理的帰結 形式的証明 命題論理体系の健全性と完全性

論理による問題解決 論理式による知識の表現 証明(推論)による解決 知識 (論理式の集合) 推論規則 結論(答)

論理による問題解決 太郎は花子の父である. 次郎は太郎の父である. 父の父は祖父である. 推論規則

命題論理:構文 論理式 原子式,論理記号 整式(well-formed formula wff) (1) 原子式は整式である. 論理式    原子式,論理記号 整式(well-formed formula wff) (1) 原子式は整式である. (2)  は整式である ⇒    は整式である. (3) ,  は整式である ⇒     は整式である. (4) 以上(1),(2),(3) より整式とわかるものだけが整式である. 論理記号 否定(negation) 連言(conjunction) 選言(disjunction) 含意(implication)

命題論理:意味 解釈: 原子式への真(T),偽(F)の割り当て 原子式 と解釈  : 論理記号の意味(真理表) T F

論理式の解釈 p q r T F p q r T F

同値関係 二重否定の法則(law of double negation): べき等律(idempotent law): 相補律(complementary law): 交換律(commutative law): 結合律(associative law): 分配律(distributive law): ド・モルガンの法則(De Morgan’s law): (矛盾律) (排中律)

標準形 節形式(clausal form) (連言標準形(conjunctive normal form CNF)) リテラル(literal): 原子式またはその否定形 節(clause): リテラルの選言 節形式: 節の連言 リテラル 節

節形式への変換 (1)含意記号を除去する. (2)否定記号を原子式の直前に移動する. (3)分配律を適用する.

恒真式と恒偽式 論理式全体 恒真式 恒偽式 充足可能 充足不能

決定問題 決定問題(decision problem) 意味木(semantic tree) 所与の論理式が恒真か否かを決定する問題 → 命題論理式の場合,有限時間で決定可能 意味木(semantic tree)

意味木 p q T F

推論 推論(inference, reasoning) 前提(premise)から結論(conclusion)を導くこと 前提① 前提② 前提① 鳥は卵を産む. 前提② 鶏は鳥である. 結論   鶏は卵を産む. 前提① 鳥は卵を産む. 前提② 猫は鳥である. 結論   猫は卵を産む. 前提① 前提② 結論 健全(sound)な推論 妥当(valid)な推論

推論の形式(推論規則) 肯定式(modus ponendo ponens) 否定式(modus tollend tollens) 三段論法(syllogism) (前提) (結論) (前提) (結論) (前提) (結論)

推論の妥当性 論理的帰結(logical consequence) 前提 が真となる任意の解釈において 結論 も真となる. (前提)   前提            が真となる任意の解釈において   結論   も真となる. (前提) (結論)

論理的帰結 :恒真 :恒偽 :充足不能

推論規則と恒真式 推論規則 恒真式 前件肯定規則 前提 結論 前件肯定式 対偶法 対偶律 選言除去規則(Dilemma規則) 選言除去式 選言三段論法 選言三段論法式 仮言三段論法 推移律

形式的証明 演繹体系 恒真式の集合 公理系 定理 推論規則 恒真式 妥当な推論

証明可能 形式的証明   公理系+推論規則 → 仮説からの演繹   公理+仮説  +推論規則 → 演繹定理

命題論理体系の性質 公理系の無矛盾性(consistency) いかなる論理式 についても と が 健全性(soundness)   いかなる論理式  についても  と   が    ともに証明可能となることはない. 健全性(soundness) 完全性(completeness)