第7回　 命題論理.

Presentation on theme: "第7回　 命題論理."— Presentation transcript:

1 第7回　 命題論理

2 述語論理(predicate calculus, logic)知識を記号の式として数学的に表現
知識表現の種類と特徴-７　 　述語論理(predicate calculus, logic)知識を記号の式として数学的に表現 cf）述語：　真偽判定可能な叙述 例）　(∀Ｘ)(elephant(X) → color(X, gray)) 理論的基盤が保証されている 導出原理(resolution principle)による推論 人間の持つ曖昧性を組み込むことが困難

3 数理論理学 ←哲学 対象： 恒真命題・ 恒偽命題 論理式により近似された人間の思考の言語的側面と，
世界を代数モデルで近似した世界モデルとの関係を分析 命題論理： 数理論理学の 基本的な枠組み 対象： 恒真命題・ 恒偽命題 世界がどこまで記述できるか？　どのような推論が実現できるか？

4 基本的な概念 -1 論理式： 自然言語の文に相当 意味論 論理式とモデルがどのように対応付けられるかを規定
基本的な概念　-1 論理式：　自然言語の文に相当 意味論 論理式とモデルがどのように対応付けられるかを規定　 統語論 論理式がどのようにして構成されるか（どのような記号列が論理式として許容されるか）を規定 　-命題記号　 -論理的接続詞: ∧(AND)，∨(OR)，￢(NOT)，≡ -複合命題

5 基本的な概念 -2 意味論 1) 意味領域を規定 真理値{0,1} 1:真(true) ０：偽(false)
基本的な概念　-2 意味論 1) 意味領域を規定 　真理値{0,1} 　1:真(true)　０：偽(false) 　2) 意味写像を規定 　統語論で規定された論理式を 　意味領域のオブジェクトに対応付け 　　論理定数　Ｔ（意味値1に固定），Ｆ（意味値0に固定） 　 ３) 意味写像に自由度を持たせる 　～　異なる意味写像は，文脈・状況を反映

6 定理証明の方法 意味論的アプローチ 意味論による論理式の意味定義に基づき，与えられた論理式の恒真性を直接的に証明 ～論理的帰結 α|=β
意味論的アプローチ 意味論による論理式の意味定義に基づき，与えられた論理式の恒真性を直接的に証明 ～論理的帰結　 α|=β 証明論的アプローチ 意味論に直接言及せず，論理式の変換操作だけによって恒真性を示す手法 ～証明　 α|-β

7 基本的な概念　-3 健全(sound): 証明論的方法で恒真性を示した命題が，常に， 意味論的にも恒真性を保証されている場合 α|-β →　 α|=β 完全（complete): 意味論的に恒真の論理式が与えられた場合， それが恒真であることを導く論理式操作（証明論的手法）が常に存在する場合 α|=β →　 α|-β 複雑な論理体系～　健全だが不完全

8 命題論理を用いた論証例：問題 「明日，雨でなければハイキングに行く」 「明日，雨であれば水族館に行く」
「ハイキング，水族館に行くことは遊びに行くこと」 →　「明日は遊びに行く」

9 命題論理を用いた論証例：方式 前提） ・ ￢R → H ・R → A ・(H → X) ∧ (A → X) 結論） Ｘ
　　命題論理を用いた論証例：方式 ・Ｒ：「明日は雨である」 ・Ｈ：「明日はハイキングに行く」 ・Ａ：「明日は水族館に行く」 ・Ｘ：「明日は遊びに行く」 前提） ・ ￢R → H ・R → A ・(H → X) ∧ (A → X) 結論） 　Ｘ

10 命題論理の体系： 統語論 命題記号： 定義命題を表すために用いる記号 論理式： 命題記号は論理式 Gが論理式なら，￢ Gも論理式
命題論理の体系：　統語論 命題記号：　定義命題を表すために用いる記号 論理式： 命題記号は論理式 Gが論理式なら，￢ Gも論理式 G, Hが論理式なら， G ∨ H, G ∧ H, G → H, G≡H も論理式 リテラル：　命題記号またはその否定

11 命題論理の体系： 意味論 命題論理式Fの解釈I [F]I： Ｆが命題記号Gのとき， [F]I =[G]I
命題論理の体系：　意味論 命題論理式Fの解釈I　[F]I： Fの中に出現する命題記号Ａｉの真理値{0,1}への割り当て方 Ｆが命題記号Gのとき，　[F]I =[G]I F= ￢Gのとき，[F]I =[￢G]I =1-[G]I Ｆが複合命題式の場合は，真理値表により 決定 FはＩのもとで真： 論理式Ｆ，解釈Ｉに対し， [F]I =1 Fは恒真： 全ての解釈Ｉに対し， [F]I =1

12 複合命題の真理値表 一致

13 等価命題

14 節形式 素（原子）命題： 述語記号と項から構成される命題 リテラル(literal)： 素命題、または素命題の否定
素（原子）命題：　述語記号と項から構成される命題 リテラル(literal)：　素命題、または素命題の否定 節(clause)：リテラル、またはリテラルの選言 ・連言標準形: G1∧ G２∧ ・・∧Gn ・選言標準形: G1∨ G2 ∨ ・・∨Gn

15 節形式への変換(等価変換） P → Qを￢P∨Qに、 Ａ≡Ｂを（￢Ａ∨Ｂ）∧（￢Ｂ∨Ａ）に変換
否定記号の括り出し： ￢（￢Ａ）=Ａ ￢（Ａ∧Ｂ）= （￢Ａ∨￢Ｂ） ￢（Ａ∨Ｂ）= （￢Ａ∧￢Ｂ） 分配法則を用いて、母式を選言の連言結合形に変換： （Ａ∧Ｂ）∨（Ｂ∧C）=（Ａ∨Ｂ）∧ （Ｂ∨C）∧Ｂ∧（Ａ∨C） P∨（Q∧R）=（P∨Q）∧（P∨R） P∧（Q ∨ R）=（P∧Q）∨（P∧R）

16 意味論的アプローチ 真理値表の利用 全ての解釈（2n)について真となっているかを 真理値表で確認
Quineのアルゴリズム 全ての解釈を場合分けにより系統的に調査 例）(￢P∧￢Q ∧R)∨(￢P∧Q)∨P∨￢R∨￢U の恒真性？

17 例）の真理値表による解法 16通り

18 例）のQuineのアルゴリズムによる解法

19 証明論的アプローチ 命題の恒真（偽）性を，公理(axiom) αと 推論規則(inference rule)により導出
定理F:　以下を満足するSが存在 ＦはSの最後の命題論理式 Sのどの命題論理式も，公理αであるか， それより前の命題論理式から推論規則の一つを用いて導かれるかのいずれか S: Fの証明　　 α|-　F 健全かつ完全であることを証明しておかねばならない

20 証明論的アプローチの手法-1 論理式の変形

21 等価変換の例

22 証明論的アプローチの手法-２ 自然演繹法（Gentzen) 与えられた命題論理式と以下の３つの公理を起点とし，証明を積み重ねることにより， 定理証明を実施 Γ：任意の命題論理式の集合，A,B:任意の命題論理式 仮言公理：　Γ, A |- A 仮定の導入： Γ |- B →　 Γ, A |- B 仮定の除去：　 Γ, A |- B， Γ, ￢A |- B → Γ |- B

23 自然演繹法の具体例 仮言公理 ∨導入 仮定除去

24 証明論的アプローチの手法-３ Davis-Putnum法： 以下の４つの規則を再帰的に使ってSの充足不能(恒偽)性を証明 １．トートロジー(いかなる解釈のもとでも真となる表現）規則：　無関係部分の除去 ２．１リテラル規則：　融合原理 ３．純粋（その否定がどの節にも現れない）リテラル規則：　無関係部分の除去 ４．分割規則：　融合原理

25 Davis-Putnum法の適用例 → 充足不能 （P ∨ Q ∨ ￢R） ∧ （P ∨ ￢Q ） ∧ ￢P ∧R ∧ U ： 前提
（Q ∨ ￢R） ∧ ￢Q ∧R ∧ U　：　￢Pに関する１リテラル規則 ￢R∧ R ∧ U　：　￢Qに関する１リテラル規則 F ∧ U　：　 Rに関する１リテラル規則 →　充足不能

26 融合原理 (mechanical theorem proving method)
第8回　 命題論理 融合原理 (mechanical theorem proving method) 　　任意の２つの節C1，C2に対して，C1がリテラルLを含み，C2が￢Lを含むとき，C1からLを除いた部分とC2から￢Lを除いた部分を合せて作った節を融合節Cと呼ぶ． このCはC1とC2の論理的帰結である． ～　Davis-Putnum法における １リテラル規則の拡張

27 第8回　 命題論理 mutty@ics.kagoshima-u.ac.jp
節の融合の具体例

28 命題論理の体系：原理 原理： 公理系に推論規則を適用して定理を導く
第8回　 命題論理 命題論理の体系：原理 原理：　公理系に推論規則を適用して定理を導く 完全性定理(completeness theorem): 定理は全て恒真であり，その逆も成立 ←　公理は恒真式であり，推論規則は健全 公理系の無矛盾性(consistency): いかなる論理式Pに対しても，Pと￢Pが同時に証明可能となることはない