研究テーマ：状況・状態把握技術

第7回
命題論理
1
知識表現の種類と特徴-７
述語論理(predicate calculus, logic)
知識を記号の式として数学的に表現
cf）述語：真偽判定可能な叙述
例） (∀Ｘ)(elephant(X) → color(X, gray))



理論的基盤が保証されている
導出原理(resolution principle)による推論
人間の持つ曖昧性を組み込むことが困難
2
数理論理学 ←哲学
論理式により近似された人間の思考の言語的側面と，
世界を代数モデルで近似した世界モデルとの関係を分析
命題論理：
数理論理学の
基本的な枠組み
対象：
恒真命題・
恒偽命題
世界がどこまで記述できるか？どのような推論が実現できるか？
3
基本的な概念 -1
論理式：自然言語の文に相当
 意味論
論理式とモデルがどのように対応付けられるか
を規定
 統語論
論理式がどのようにして構成されるか（どのよう
な記号列が論理式として許容されるか）を規定
-命題記号
-論理的接続詞: ∧(AND)，∨(OR)，￢(NOT)，≡
-複合命題
4
基本的な概念 -2

意味論
1) 意味領域を規定
真理値{0,1} 1:真(true) ０：偽(false)
2) 意味写像を規定
統語論で規定された論理式を
意味領域のオブジェクトに対応付け
論理定数Ｔ（意味値1に固定），Ｆ（意味値0に固定）
３)
意味写像に自由度を持たせる
～異なる意味写像は，文脈・状況を反映
5
定理証明の方法

意味論的アプローチ
意味論による論理式の意味定義に基づき，与え
られた論理式の恒真性を直接的に証明
～論理的帰結 α|=β

証明論的アプローチ
意味論に直接言及せず，論理式の変換操作だ
けによって恒真性を示す手法
～証明 α|-β
6
基本的な概念 -3

健全(sound):
証明論的方法で恒真性を示した命題が，常に，
意味論的にも恒真性を保証されている場合
α|-β → α|=β
完全（complete):
意味論的に恒真の論理式が与えられた場合，

それが恒真であることを導く論理式操作（証明論
的手法）が常に存在する場合
α|=β → α|-β
複雑な論理体系～健全だが不完全
7
命題論理を用いた論証例：問題
「明日，雨でなければハイキングに行く」
「明日，雨であれば水族館に行く」
「ハイキング，水族館に行くことは遊びに行くこと」
→ 「明日は遊びに行く」
8
命題論理を用いた論証例：方式
・Ｒ：「明日は雨である」
・Ｈ：「明日はハイキングに行く」
・Ａ：「明日は水族館に行く」
・Ｘ：「明日は遊びに行く」
前提）
・￢R → H
・R → A
・(H → X) ∧ (A
結論）
Ｘ
→
X)
9
命題論理の体系：統語論
命題記号：定義命題を表すために用いる記号
論理式：
1.
命題記号は論理式
2.
Gが論理式なら，￢ Gも論理式
3.
G, Hが論理式なら，
G ∨ H, G ∧ H, G → H, G≡H
も論理式
リテラル：命題記号またはその否定
10
命題論理の体系：意味論
命題論理式Fの解釈I [F]I：
Fの中に出現する命題記号Ａｉの真理値{0,1}への割り当て方
Ｆが命題記号Gのとき， [F]I =[G]I
2.
F= ￢Gのとき，[F]I =[￢G]I =1-[G]I
3.
Ｆが複合命題式の場合は，真理値表により
決定
FはＩのもとで真：
論理式Ｆ，解釈Ｉに対し， [F]I =1
Fは恒真：
全ての解釈Ｉに対し， [F]I =1
1.
11
複合命題の真理値表
一致
12
等価命題
13
節形式

素（原子）命題：
述語記号と項から構成さ
れる命題

リテラル(literal)：
素命題、または素命題
の否定

節(clause)：リテラル、またはリテラルの選言
・連言標準形: G1∧ G２∧ ・・∧Gn
・選言標準形: G1∨ G2 ∨ ・・∨Gn
14
節形式への変換(等価変換）
1.
2.
3.
P → Qを￢P∨Qに、
Ａ≡Ｂを（￢Ａ∨Ｂ）∧（￢Ｂ∨Ａ）に変換
否定記号の括り出し：￢（￢Ａ）=Ａ
￢（Ａ∧Ｂ）= （￢Ａ∨￢Ｂ）
￢（Ａ∨Ｂ）= （￢Ａ∧￢Ｂ）
分配法則を用いて、母式を選言の連言結合形
に変換：
（Ａ∧Ｂ）∨（Ｂ∧C）=（Ａ∨Ｂ）∧ （Ｂ∨C）∧Ｂ∧（Ａ∨C）
P∨（Q∧R）=（P∨Q）∧（P∨R）
P∧（Q ∨ R）=（P∧Q）∨（P∧R）
15
意味論的アプローチ


真理値表の利用
全ての解釈（2n)について真となっているかを
真理値表で確認
Quineのアルゴリズム
全ての解釈を場合分けにより系統的に調査
例）(￢P∧￢Q ∧R)∨(￢P∧Q)∨P∨￢R∨￢U
の恒真性？
16
例）の真理値表による解法
16通り
17
例）のQuineのアルゴリズムによる解法
18
証明論的アプローチ
命題の恒真（偽）性を，公理(axiom) αと
推論規則(inference rule)により導出
定理F: 以下を満足するSが存在
1.
ＦはSの最後の命題論理式
2.
Sのどの命題論理式も，公理αであるか，
それより前の命題論理式から推論規則の一つ
を用いて導かれるかのいずれか
S: Fの証明
α|- F
健全かつ完全であることを証明しておかねば
ならない
19
証明論的アプローチの手法-1

論理式の変形
20
等価変換の例
21
証明論的アプローチの手法-２

自然演繹法（Gentzen)
与えられた命題論理式と以下の３つの公理を
起点とし，証明を積み重ねることにより，
定理証明を実施
Γ：任意の命題論理式の集合，A,B:任意の命題論
理式
1.
仮言公理： Γ, A |- A
2.
仮定の導入： Γ |- B → Γ, A |- B
3.
仮定の除去： Γ, A |- B， Γ, ￢A |- B →
Γ |- B
22
自然演繹法の具体例
仮言公理
∨導入
仮言公理
∨導入
仮定除去
23
証明論的アプローチの手法-３

Davis-Putnum法：
以下の４つの規則を再帰的に使ってSの
充足不能(恒偽)性を証明
１．トートロジー(いかなる解釈のもとでも真とな
る表現）規則：無関係部分の除去
２．１リテラル規則：融合原理
３．純粋（その否定がどの節にも現れない）リテ
ラル規則：無関係部分の除去
４．分割規則：融合原理
24
Davis-Putnum法の適用例
（P ∨ Q ∨ ￢R） ∧ （P ∨ ￢Q ） ∧ ￢P ∧R ∧ U ：
前提
（Q ∨ ￢R） ∧ ￢Q ∧R ∧ U ：￢Pに関する１リテラル規則
￢R∧ R
∧U ：
￢Qに関する１リテラル規則
F ∧ U ： Rに関する１リテラル規則
→ 充足不能
25
第8回命題論理
[email protected]
融合原理 (mechanical theorem proving method)
任意の２つの節C1，C2に対して，C1がリ
テラルLを含み，C2が￢Lを含むとき，C1
からLを除いた部分とC2から￢Lを除いた
部分を合せて作った節を融合節Cと呼ぶ．
このCはC1とC2の論理的帰結である．
～ Davis-Putnum法における
１リテラル規則の拡張
26
第8回命題論理
[email protected]
節の融合の具体例
27
第8回命題論理
[email protected]
命題論理の体系：原理
原理：公理系に推論規則を適用して定理を導く
 完全性定理(completeness theorem):
定理は全て恒真であり，その逆も成立
← 公理は恒真式であり，推論規則は健全
 公理系の無矛盾性(consistency):
いかなる論理式Pに対しても，Pと￢Pが同時に証
明可能となることはない
28

Download Report