情報実習II

数理論理学
第15回
タブローの方法
© 加藤，高田，新出
2.4節(p. 23)
タブローの方法
S=
{parent(hiroshi,maruko),
C1
male(hiroshi),
C2
father(x,y)∨￢parent(x,y)∨￢male(x) C3}
} を節集合とする。
課題14-1 S に対するエルブラン基底
(要素10個)を求めよ。
課題14-2 S に対するエルブラン解釈
HI = {parent(hiroshi,maruko), male(hiroshi), father(hiroshi, maruko)}.
がエルブランモデルであることを証明せよ。
S={parent(hiroshi,maruko),
C1 解答
male(hiroshi),
C2
father(x,y)∨￢parent(x,y)∨￢male(x) C3}
HUs = {hiroshi, maruko}
HBS =
{
parent(hiroshi,hiroshi),parent(hiroshi,maruko),
parent(maruko,hiroshi), parent(maruko,maruko),
male(hiroshi), male(maruko),
father(hiroshi,hiroshi),father(hiroshi,maruko),
father(maruko,hiroshi), father(maruko,maruko)
}
Sの一つのエルブラン解釈 HI を以下のように取るとき、
HI = {parent(hiroshi,maruko), male(hiroshi), father(hiroshi, maruko)}.
この HI が S のエルブランモデルであることを証明する。
parent(hiroshi,maruko)∈HI より、
HI({parent(hiroshi,maruko)})= T 。
同様に、 HI (male(hiroshi))= T 。
次に、節C3= father(x,y)∨￢parent(x,y)∨￢male(x)
に対して、各変数に HUs の全ての組み合わせを代入した
場合の各 HI({C3θ}) の値を求める。
代入θ={hiroshi/x, hiroshi/y} の場合:
parent(hiroshi, hiroshi) ∈HI より
HI({parent(hiroshi, hiroshi)}) =⊥。よって定義3.17 (p. 61)の
2より、 HI({￢(parent(hiroshi, hiroshi)}) = T 。 a
よって、定義3.17の4 (p. 62)より、 HI({C3θ}) = T 。
b
代入θ ={hiroshi/x, maruko/y} の場合:
father(hiroshi, maruko) ∈HIより
HI ({father(hiroshi, maruko)}) = T c 。よって、定義3.17の
4より、Val(C3θ)= T d 。
代入θ = θ3 ={maruko/x, hiroshi/y}と
θ = θ4 ={maruko/x, maruko/y}の場合:
e
male(maruko) ∈HI より HI({male(maruko)})= ⊥ 。
よって定義3.17の2より、 HI({￢ male(maruko)}) = T f 。
よって定義定義3.17の4より、 HI({C3θ3})= HI({C3θ4})= T g。
以上より、全ての組み合わせに対してC3の値はTになる。
よって定義3.17の6より、 HI ({C3})= T h。
以上より、エルブラン解釈HIは、節集合 S 中の全ての節
の値をTにするので、定義3.17の3より、 HI (S)= T i 。
HI(S)= Tとなるエルブラン解釈はSのエルブランモデル j
なので、 HIは Sのエルブランモデル j である。
モデルによる充足不能判定
導出原理による充足不能判定
どんな解釈
導出原理によって
I を使っても
空節が得られる
I(S)= ⊥
定理4.4 導出原理の健全性と完全性 (p. 104)
エルブランの定理 (p. 110 定理 4.3)
どんな解釈、つまり無限にあるあらゆる
定義4.16 エルブラン領域 (p. 105)
解釈を扱い証明することは困難
定義4.17 エルブラン基底 (p. 105)
定義4.18 割り当てAS (p. 105)
定義4.19 エルブラン解釈とエルブランモデル(p. 107)
2.4 (命題論理の)タブローの方法
(p. 23)
命題論理 (p. 9) 変数を含まない論理式
定義2.1(p. 10)
命題変数
p: 雨が降っている (p. 10)
q: 傘をさすべきである
p: 気温が低い
q: セーターを着るべきである
pq
その他の定義は
述語論理と同様
論理演算子(定義2.2), 論理式(定義2.3),
(pp. 10-13)
部分論理式(定義2.4), 演算子間の優先順位(定義2.5)
2.2 命題論理の意味論
定義 2.7 真理値割り当て (p. 16)
A : P →B（命題変数の集合から真理値の集合への関数)
2.2 命題論理の意味論
定義 2.8 命題論理の解釈 (p. 17)
IA : Epro →B（論理式の集合から真理値の集合への関数)
例2.4 (4) (p. 18) A5: p1 T , p2 ⊥, p3 T の場合
IA(p1 ∧p2 ⊃p3) = T
複雑な論理式では
計算が困難
2.4 タブローの方法 (p. 23)
複雑な論理式でも機械的に恒真性の
証明が可能な方法
証明したい式の否定から始め矛盾を導く（pp. 23, 24
 ⊥:
 ⊥:
p ∨￢p
p
 ⊥: ￢p
T: p

例2.7)
2.4 タブローの方法 (p. 23)
複雑な論理式でも機械的に恒真性の
証明が可能な方法
証明したい式の否定から始め矛盾を導く（pp. 23, 24
 ⊥:
 ⊥:
p ∨￢p
p
(⊥: p ∧ ⊥ : ￢ p)
同じ p に対して
⊥: と T:
がついている
 ⊥: ￢p
 T符: p
マ既号
ー分
ク解  矛盾していることの目印
例2.7)
定義2.14 節点，
節点，枝，根，葉，道 (p. 25)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
節点
定義2.14 節点，枝，根，葉，道 (p. 25)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
根
定義2.14 節点，枝，根，葉，道 (p. 25)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
葉
定義2.14 節点，枝，根，葉，道 (p. 25)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
枝
定義2.14 節点，枝，根，葉，道 (p. 25)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
道
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
s
F :節点
s
leaf
F :葉
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
s
F :節点
s
leaf
F :葉
0
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
 ⊥:
p ∨・・・
s
( F) T : ￢E
s
leaf
F
s
F :節点
s
leaf
F :葉
⊥: E
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
s
F :節点
s
leaf
F :葉
0
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
分岐型
 ⊥:
p ∨・・・
( F) ⊥: E1∧ E2
s
 0 :木
s
leaf
F
s
F :節点
s
leaf
F :葉
⊥: E1
⊥: E2
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
s
F :節点
s
leaf
F :葉
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
s
F :節点
s
leaf
F :葉
0
定義2.16
(pp. 27,28)
節点の
種類別
構成規則
 0 :木
 ⊥:
p ∨・・・
( F) ⊥: E1⊃ E2
s
s
leaf
F
s
F :節点
s
leaf
F :葉
T : E1
⊥: E2
例2.8
(p. 29)
 ⊥:
p ∨￢p
 ⊥:
p
 ⊥: ￢p
T: p
規則 6
規則 2
 矛盾していることの目印
例2.9  ⊥: ((p ⊃q) ⊃p) ⊃p
規則 8
(p. 31)
 T : (p ⊃q) ⊃p
規則 7
 ⊥: p
⊥: p ⊃q
T : p

規則 8
T:p

練習問題下記の論理式が恒真であることを証明せよ
: ( p  ( p  q))  q
練習問題下記の論理式をタブローの方法により証明せよ
: ( p  ( p  q))  q
T : p  ( p  q)
:
練習問題下記の論理式をタブローの方法により証明せよ
 : ( p  ( p  q))  q 規則 8
規則 3
 T : p  ( p  q)
 : q
 T : p
規則
7
:
p

q
 T
 : p

 T: q

練習問題下記の論理式をタブローの方法により証明せよ
 : ( p  ( p  q))  q 規則 8
規則 3
 T : p  ( p  q)
 : q
 T : p
規則
7
:
p

q
 T
 : p

 T: q

課題15 次の論理式の恒真性を
タブローの方法により証明せよ
( p  p)  q
: ( p  p)  q
T :
:
課題15 正解
 ⊥:
(p ∧￢p)⊃q
 T : p ∧￢p
 ⊥:
規則 8
規則 3
q
T : p
 T : ￢p
⊥: p

規則 1

Download Report