H28ヒント集

H28ヒント集
一階述語論理式
•  全称限量の基本（∀→）
「人は死ぬ。(Manismortal.)」
∀x(Man(x)→Mortal(x))
•  存在限量の基本（∃∧）
「死なない人がいる。(Thereisamanwhois
notmortal.)」
∃x(Man(x)∧¬Mortal(x))
一階述語論理式
•  存在限量∃は∧と相性がよい
「AでBのものがある」
「BなるAがある」
（正）　∃x(A(x)∧B(x))
（誤）　∃x(A(x)→B(x))　…よくある間違い
一階述語論理式
•  存在の否定は、∀で言い換えてみよう
「どんなAもBでない」
¬∃x(A(x)∧B(x))
⇔∀x¬(A(x)∧B(x))
⇔∀x(¬A(x)∨¬B(x))
⇔∀x(A(x)→¬B(x))　…分かりやすいかも
一階述語論理式
•  部分否定は、∃で言い換えてみよう
「すべてのAがBというわけではない」
¬∀x(A(x)→B(x))
⇔∃x(A(x)∧¬B(x))
一階述語論理式
•  only
「AだけがB。(OnlyAisB.)」
∀x(B(x)→A(x))…語順が逆なので注意
一階述語論理式
•  if,onlyif,ifandonlyif
「AifB」
∀x(B(x)→A(x))　…英語と語順が逆
「 AonlyifB」
∀x(A(x)→B(x))　…英語の語順通り
「AifandonlyifB」
∀x(A(x)⇔B(x))
一階述語論理式
•  ∀や∃を同値変形して検討しよう
¬∀xΨ(x)
⇔∃x¬Ψ(x)
¬∃xΨ(x)
⇔∀x¬Ψ(x)
¬Ψ(x)をド・モルガン則で同値変形するなど
一階述語論理式
•  全称限量∀xでは領域を意識しよう
「AはB」
∀x(A(x)→B(x))
xは人間とは限らない。
−1
（虫や石ころや虚数単位　かもしれない。）
A(x)が対象を限定していればOK
タブロー法
•  ひたすら論理式を分解していく
（論理結合子をはずしていく）
•  枝が単に伸びるα型分解
例）　i行目　T：　φ∧Ψ
：
：
j行目　T:　φ　αi
j+1行目　T：　Ψ　αi
タブロー法
•  枝が単に伸びるα型分解
（基本）　T：　φ∧Ψ　（T:φと T:Ψで伸ばす）
ほかにも
F: φ∨Ψ　（F:φ とF:Ψで伸ばす）
F: φ→Ψ　（T:φとF:Ψで伸ばす）
タブロー法
•  枝が２本に分岐するβ型分解
例）　i行　T：　φ∨Ψ
：
：
βi
j行　T:　φ　j+1行　T：　Ψ
•  木構造ができていく
タブロー法
•  枝が２本に分岐するβ型分解
（基本）　T：　φ∨Ψ　（T:φと T:Ψで分岐）
ほかにも
F:　φ∧Ψ　（F:φとF:Ψで分岐）
T:　φ→Ψ　（F:φとT:Ψで分岐）
タブロー法
•  同じ式（基本は命題変数）にT：とF：がつけば
枝が閉じる
例）　i行　T：　φ
：
：
j行　F:　φ
×i,j
((p→(q∨r))∧(q→s)∧(r→t))→(p→(s∨t))
1F:((p→(q∨r))∧(q→s)∧(r→t))→(p→(s∨t))n.o.c.
2T:(p→(q∨r))∧(q→s)∧(r→t)1
3F:p→(s∨t)1
4T:p→(q∨r)2
5T:q→s2
6T:r→t2
7T:p3
8F:s∨t3
9F:s8
10F:t8
4
11  F:p12T:q∨r
X7,1112
13T:q14T:r
56
15F:q16T:s17F:r18T:t
X13,15X9,16X14,17X10,18
ResoluYon法
•  与えられた式をCNFに変換する
例）　p∨（q∧r）
⇒(p∨q）∧（p∨r）
節
節
ResoluYon法
•  CNFへの変形規則
–  含意
x→y⇒¬x∨y
–  分配 x∨(y∧z)⇒(x∨y)∧(x∨z)
–  ドモルガン¬(x∨ｙ)⇒¬x∧¬y
¬(x∧ｙ)⇒¬x∨¬y
–  ２重否定¬¬x⇒x
ResoluYon法
•  前提１，…，前提n　結論
–  各前提iごとにCNF変換　⇒節集合Si
–  結論の否定をCNF変換⇒節集合Sc
–  節集合の和 S=S1∪…∪Sn∪Sc
ResoluYon法
•  節集合 S から2つの節を選んでresoluYon
例）　{…p∨q,…,¬p∨r,…}
q∨r
•  結果（resolvent）をSに追加
•  この過程を繰り返す
ResoluYon法
•  目指す最後のresoluYon
例）　{…p,…,¬p,…}
□　（矛盾）
ResoluYon法
•  resoluYon過程の線形表現
例） S={p,¬p∨q,¬q}　に対して、
1p　∈S
2¬p∨q　∈S
3¬q　∈S
4qres.1,2
5□res.3,4
(p→(q∨r)),(q→s),(r→t)(p→(s∨t))
前提１のCNFp→(q∨r)⇒¬p∨q∨r
前提２のCNFq→s⇒¬q∨s
前提３のCNFr→t⇒¬r∨t
結論の否定のCNF¬(p→(s∨t))⇒¬(¬p∨s∨t)⇒p∧¬s∧¬t
1  ¬p∨q∨r∈S
2  ¬q∨s∈S
3  ¬r∨t∈S
4  p∈S
5  ¬s∈S
6  ¬t∈S
7  q∨rres.1,4
8  ¬qres.2,5
9  ¬rres.3,6
10  rres.7,8
11  □res.9,10
自然演繹法
•  前提に現れるφ→Ψは、→e規則で分解するよ
うに努める
–  Ψが役に立つはずだから
–  φがなければassumeしよう
•  結論に現れるφ→Ψは、→i規則で作り出すよ
うに努める
–  何はともあれ、φをassumeしよう
–  Ψはきっと導けるはず
自然演繹法
(p→(q∨r)),……
1  p→(q∨r)prem
2  …
3  pass
4  q∨r→e1,2
5  …
...
自然演繹法
•  前提に現れるφ∨Ψは、∨e規則で分解するよ
うに努める
–  別の欲しい χがΦとΨのそれぞれから導けるはず
(p→(q∨r)),(q→s),(r→t)(p→(s∨t))
1  p→(q∨r)prem
2  q→sprem
3  r→tprem
4  pass
5  q∨r→e1,4
6  qass
7  s→e2,6
8  s∨t∨i7
9  rass
10  t→e3,9
11  s∨t∨i10
12  s∨t∨e5,6-8,9-11
13  p→(s∨t)→i4-12
自然演繹法
•  MT規則を使ってみよう
i行めp→q
j行め ¬q
k行め¬pMTi,j
自然演繹法
(p→q)(¬q→¬p)
1  p→qprem
2  ¬qass
3  ¬pMT1,2
4  ¬q→¬p→i2-3
自然演繹法
•  「苦しいときのLEM頼り」
やることがまったく思いつかないときは、
役に立ちそうなΨを思い浮かべて
i行め　Ψ∨¬Ψ　LEM
と書き、∨e規則の適用に持ち込もう
（LEMと∨eはワンセット）
ブール方程式
•  y1,y2に関する連立方程式
L1=R1
L2=R2
•  F(y1,y2)を作る
F(y1,y2)=L1’・R1+L1・R1’+L2’・R2+L2・R2’
•  F(0,0),F(1,0),F(0,1),F(1,1)を計算
•  F(0,0)・F(1,0)・F(0,1)・F(1,1)=0を確認
ブール方程式
•  y2の一般解
y2=F(0,0)・F(1,0)+α2・(F(0,1)・F(1,1))’
•  F(0,y2),F(1,y2)を計算
（y2には上の一般解を代入）
•  y1の一般解
y1=F(0,_)+α1・F(1,_)’
ブール方程式
•  式の簡約化
x+x’・y
=x・(1+y)+x’・y
=x・1+(x+x’)・y
=x+1・y
=x+y

Download Report