8.不完全な知識

8.不完全な知識
新しい知識が追加されたとき、
これまでの知識との
整合性がとれなくなる…
論理体系の単調性と非単調性
単調性
:
非単調性 :
矛盾のない命題(公理)の集合Aから証明さ
れた命題(定理)の集合をTh(A)とし、Aに新し
い公理を付け加えた結果の集合Bから証明さ
れた定理の集合をTh(B)とすると
A⊂B ならば Th(A)⊂Th(B)
集合Aに例外を含む知識(公理)が存在する
場合、必ずしも Th(A)⊂Th(B) は成立しな
い。成立しない場合の論理体系を非単調論
理(Nonmonotonic Logic)と呼ぶ。
閉世界仮説
Closed World Assumption
閉世界
:
開世界
:
与えられた情報が世界の全てであり、それ以上の情報
は得られない。
P(x)が証明できなければ~P(x)
(実世界)後で情報が付け加えられる。
カード a, b, c が赤色のカードであるという事実
赤色(a)∩赤色(b)∩赤色(c)
があるとき、次のカード d が赤色であるかどうかは分からない。閉世界
仮説では、
赤色(d)が証明されないので、~赤色(d)
とする。あくまで「仮説」である。
8.1 サーカムスクリプション
Circumscription

例外を含む知識を扱うために、知識の適用範囲を限定する方法
興味のある人のために…
事実
赤(a)∩赤(b)∩赤(c)
①
が成立するとき、~赤(d)であるということは、
∀x[赤(x)→(x = a ∪ x = b ∪ x = c)]
②
ここで x = a とは、述語 Equal(x, a)であり、x と a が等しいときに True となる。
①と②から
∀x[(x = a ∪ x = b ∪ x = c) →赤(x) ]
→ ∀x[赤(x)→(x = a ∪ x = b ∪ x = c)]
一般化して、
∀x[Φ(x) →P(x) ]→ ∀x[P(x)→ Φ(x) ]
③
④
サーカムスクリプション=第2階述語論理の推論規則

一般には、第2階述語論理の推論を機械的に行うことは困難
興味のある人のために…
式①は述語「赤」に対する命題とみなしA(赤)として表現し、述語「赤」を一般化してΦと
すると、
A(Φ)≡Φ(a)∩Φ(b)∩Φ(c)
⑤
となる。述語「赤」のついての推論規則として次を仮定する。
A(Φ)∩(∀x)[Φ(x)→赤(x)]→(∀x)[赤(x)→Φ(x)]
⑥
一般的には、述語 P(x)に関する命題A(P)が成立している場合、その述語 P(x)をΦ
(x)で置き換えた命題を A(Φ)とするとき、
A(Φ)∩(∀x)[Φ(x)→赤(x)]→(∀x)[赤(x)→Φ(x)]
⑦
言い換えると、ある述語Φがべつの述語 A という命題を満たし、かつ「ΦならばP」であ
れば、Pが成り立つものは、Φを満足するものに限る。
8.2 デフォルト推論
Default Reasoning

Pが成立し、~Qが証明されていな
ければ、Rが成立することを、論理
記号M (Most)を用いて
P : MQ
R
と表現する。これをデフォルト(推
論)規則(Default Rule)と呼ぶ。

QとRが同じ場合、すなわち、
P : MR
R
のとき、正規デフォルト規則
(Normal Default Rule) と呼ぶ。

命題(Well-formed-formula)の
集合Wとデフォルト規則の集合D
から構成される論理体系(W, D)
をデフォルト論理体系と呼ぶ。

デフォルト規則が全て正規デフォ
ルト規則であれば、正規デフォルト
体系と呼ぶ。

デフォルト論理体系から導出され
る命題の集合を「その体系の拡張
(Extension)と呼ぶ。
デフォルト推論の例
① “Most birds fly”
Bird : M
Fly(x)
Fly(x)
② 命題集合
W
= {Penguin(x) → ~ Fly(x),
Bird(a), Bird(b), Penguin(b)}
と上記①から構成される論理体系の拡張Eは、
E
= {Penguin(x) → ~ Fly(x),
Bird(a), Bird(b), Penguin(b), Fly(a)}
論理体系の拡張の不定と不安定(1)
① はじめにどちらを適用するかで、{~P}, {~Q} のどちらになるか分からない場合
(不定)。
D=
M P , M Q
, W={}
~Q
~P
② 規則を適用すると、その規則が成り立たなくなるため、結論を取り除く必要がある
(不安定)。
D=
M P
, W={}
~P
論理体系の拡張の不定と不安定(2)
* 一般に、論理体系の拡張を求めることは簡単ではないが、拡張Eが満たす条件は以
下のとおり。
①
②
③
E0  W
Ei 1
  : M

 Th( Ei )  
 D,   Ei , ~   E 




E   Ei
i 0
E1を求めるとき、 ~P  ( E0  E1 )
が成立しても、
E2を求めた結果、 ~P  ( E0  E1  E2 ) が成立
しなくなることがあり、バックトラックしなければならない。
デフォルト推論
Default inference
正規デフォルト論理体系において、ある命題 g を直接導くこと。
デフォルト推論のアルゴリズム
①
正規デフォルト論理体系(W,D)とする。
WとCON(D)からgを証明
し、S=Wとする
PRED(D) : Dに属する前提の連言(∩)
CON(D) : Dに属する結論の連言(∩)
②
③
証明に用いたデフォルト
規則の集合をDSとする
DS={ }
(~g∩W∩CON(D)が矛盾することを示せばよい)
T
F
④
S = S ∪ CON(DS)
⑤
WとCON(D)からPRE
(DS)を証明する
⑥ S が充足可能であること
を示す
正規デフォルト体系(W,D)から命題Gを導出
W : A  G,~ A  ~B
D :d1=
C : MB
,d2=
B
~A: MC
C
ステップ②~④
まず、デフォルト規則の結論と規則の名前のリストを作成
d2を使用したので、
(B, {d1}), (C, {d2})
S = S∪CON(d2)
ステップ①
(~G, { })
ステップ②~④
(A ∪ G, { })
d1を使用したので、
S = S∪CON(d1)
すなわち、
(A , { })
(~A ∪ ~B, { })
S=(A ∪G, ~A ∪ ~B, B)
すなわち、
S=(A ∪G, ~A ∪ ~B, B, C)
ステップ⑤ d1の前提A
(A , {d1,d2 }) (~A ∪ ~B, { })
ステップ⑤ d1の前提C
(~B , { })
(~B , { d1})
(B, {d1 })
(~C , {d1 }) (C, {d2 })
(NIL , { d1, d2})
(~B , {d1,d2 }) (B, {d1, d2 })
新しい規則
を使用して
(NIL , { d1, d2}) いない
ステップ⑥ Sは変数を含まないのでSの充足可能であることは有限回で求まる。
充足可能であることの判定
命題B, C, Gが導出されることが分かっているから
次の2パターンだけを確認すれば良い。
A
T
F
B
T
T
C G
T T
T T
A∪G
T
T
~A∪~B
F
T
従って
(A, B, C, G)=(F, T, T, T)
8.3 真理性維持システム:TMS
Truth Maintenance System, Doyle 1979





推論システムから情報(信念)を受け取り、信念
間の整合性を保つ。
例外を含む知識から得られた結論は必ずしも正
しくなく、当面「信じている」だけであると考える。
結論を、「信念(Belief)」と呼ぶ。
信じている状態を「In状態」、信じていない状態を
「Out状態」と呼ぶ。
ある信念がInかOutかは他の信念の状態に依存
しており、信念の状態間の依存関係を「信念の
正当化(Justification)」と呼ぶ。
用語の導入
①それぞれの信念を「節点」とし、「接点名」、「意味」、及び「正当化」で
表現する。
節点名 意味
(正当化)
②支持リスト正当化(Support List Justification)
(SL
<In List>
<Out List>)
In List 内の全ての節点がIn状態で、Out List 内の全ての節点が
Out状態である場合に、対応する節点がIn状態になる。
③条件付正当化(Conditional Proof Justification)
(CP <Result Node> <In List>
<Out List>)
In List 内の全ての節点がIn状態で、Out List 内の全ての節点が
Out状態である場合に、<Result Node>の節点がIn状態でなけ
ればならない。
支持リスト正当化の例
「山田君は日工大情報工学科の学生である」の表現
節点名
N1
N2
N3
意味
山田は学生である
山田は日工大である
山田は情報工学科である
N4
山田は機械工学科である
正当化
(SL()())
(SL()())
(SL (N1 N2) (N4))
N4はOut状態であるため、未だ正当化されていないことに注意
信念の状態
In
In
In
Out
条件付正当化の例
節点名
N1
N2
N3
意味
スズメ → 鳥
鳥 → 飛ぶことができる
スズメである
正当化
(SL () ())
(SL () ())
(SL () ())
N4
N5
鳥である
飛ぶことができる
(SL (N1 N3) ())
(SL (N2 N4) ())
N6
スズメ → 飛ぶことができる
(CP N5 (N3) ())
N6は、N1とN2から導くことができるが、N3が成立する場合はN5も成立す
ることによって支持されている。
真理性維持の手続き
①矛盾の原因の候補となる信念を求める
②矛盾の原因の候補が求められていなけれ
ば、それが良くないという意味の節点を生
成する。
③矛盾の原因の候補から適当な信念を選ん
でOut状態にして矛盾を解消する。
信念状態の変更の過程の例(1)
打ち合わせを10時から会議室R1かR2のいずれかで行う予定
節点名
意味
正当化
信念の状態
N1
会議室=R1
(SL()(N2))
In
N2
会議室=R2
Out
N3
時刻=10時
(SL () (N4))
In
N4
時刻=13時
Out
! 推論システムが10時に部屋R1が使えないことを見つけ、TMSに伝えると
N5
矛盾
(SL (N1 N3) ())
In
!N5は矛盾節点であるのでOut状態にする。N5の原因がN1とN3であることを示す節
点を生成
N6
No good N1 N3
(CP N5 (N1 N3) ())
In
信念状態の変更の過程の例(2)
N1またはN3のどちらかをOut状態にすれば良い(N1をOutにする)
節点名
意味
正当化
信念の状態
N1
会議室=R1
(SL()(N2))
Out
N2
会議室=R2
(SL (N6 N3)())
In
N3
時刻=10時
(SL () (N4))
In
N4
時刻=13時
Out
N5
矛盾
(SL (N1 N3) ())
Out
N6
No good N1 N3
(CP N5 (N1 N3) ())
In
! 推論システムが部屋R2が使えない(N2=Out)ことを見つけ、替わりにR1を使うこと
(N1=In)がTMSに伝えられる
N7
矛盾
(SL (N2) ())
In
! N7をOutにするためにN2, N6, N3とバックトラックする。N6は変化できないこと、
N2は既にOut状態であることから、N3が良くないという信念を生成する。
N8
No good N3
(CP N7 (N3) ())
In
信念状態の変更の過程の例(3)
N3をOut状態にすれば良い
節点名
N1
N2
N3
N4
N5
N6
N7
N8
意味
会議室=R1
会議室=R2
時刻=10時
時刻=13時
矛盾
No good N1 N3
矛盾
No good N3
R1で13時から会議を行う
正当化
(SL()(N2))
(SL (N6 N3)())
(SL () (N4))
(SL (N8) ())
(SL (N1 N3) ())
(CP N5 (N1 N3) ())
(SL (N2) ())
(CP N7 (N3) ())
信念の状態
In
Out
Out
In
Out
In
Out
In
8.4 仮説に基づく真理性維持システム
ATMS:Assumption-based TMS


TMSでは、常にひとつの割り当てだけを許してい
るので、信念が成り立たないことが分かると別の
割り当てを探索しなければならないので計算量
が多くなる。
ATMSではデータがどのような仮説に基づいてい
るかという関係を記憶しておき、矛盾する部分を
取り除くことによって、真理性を維持する。
用語
① ATMSでは、TMSでの「信念」を「データ」と呼ぶ。
② データには、正しいデータ(前提)と仮説がある。
③ ATMSは、推論システムからデータとその正当化を受け取り、
節点を作成する。節点の形式は、以下のとおり。
節点名:<データ,ラベル,正当化>
④ 仮説の集合を環境(Environment)と呼び、仮説を表す節点
の集合として表現する。節点に対応する仮説の連言としての意
味を持つ。ラベルに環境を記述する。
⑤ ある節点 n が環境 E と n の正当化 J から導かれるとき、「n
は E において成立する」という。
⑥ 環境 E と 正当化 J から矛盾が導かれるとき、「E は矛盾
(Inconsistent)する」という。
考え方
① 節点 n が環境{A, B}において成立すれば、n は環境{A,
B,C}でも成立する。
② 節点 n が環境{A, B}において矛盾すれば、n は環境{A,
B,C}でも矛盾する。
③ 環境の要素である仮説の最小集合を「下界」と呼び、環境を指
定する場合、下界を指定する。
④ 節点 n のラベルに、n が成立する環境の集合を記述する。
⑤ 節点表現は、例えば次のような意味を表現する。
節点名 : <x=1, {{A, B}, {C}}, {(a), (b, c)}}>
「節点aあるいは節点bとcからx=1が導かれ、環境{A, B}と
{C}において成立する」
節点の種類
以下、小文字は節点名、大文字は仮説を示す。
①前提:前提は必ず成立するので、前提がない。
節点名:<P, {{}},{()}>
②仮説:ラベルに、仮説自身だけの環境を含む。(以下の{A})
節点名:<A, {{A}, {B, C}}, {(A), (d)}>
③仮定節点:仮説以外で、正当化が仮説であるような節点。
節点名:<b, {{A}, {B, C}}, {(A)}>
④導かれた節点:上記以外の節点
節点名:<x, {{A, B}, {C}}, {(a), (b,c)}>
表現例
(会議室の例)
節点名
N1
N2
N3
データ名(意味)
A1(会議室=R1)
A2(会議室=R2)
A3(時刻=10時)
ラベル
{{A1}}
{{A2}}
{{A3}}
正当化
{}
{}
{}
N4
A4(時刻=13時)
{{A4}}
{}
ありえない
環境の関係(24=16通
り)
{A1, A2, A3, A4}
{A1, A2, A3}
{A1, A2}
{A1, A2, A4}
{A1, A3}
{A1}
{A1, A3, A4}
{A1, A4}
{A2, A3}
{A2}
{A3}
{}
{A2, A3, A4}
{A2, A4}
{A4}
{A3, A4}
ATMSのラベル更新アルゴリズム
① 節点nの正当化が与えられると、正当化に基づいたラベルを求める。
② 正当化がp個あり、k番目の正当化がmk個の節点からなり、i番目の
節点のラベルをLikとすれば、節点nのラベルLnは
③ ラベルから冗長なものや矛盾するものを削除する。
④ 新しく得られたラベルが元のラベルと等しければ終了。
⑤ 節点nが矛盾すれば、同環境をNOGOODデータベースに追加し、
各節点のラベルから矛盾する環境を取り除く。
⑥ 節点nが矛盾しなければ、節点nを正当化に含む節点に対して、ラベ
ル変化に伴って変更を行う。
推論システムから3組のデータと正当化
<D2(場所),{(A1), (A2)}>
<D1(時刻), {(A3), (A4)}>
<E(会議), {(D1), (D2)}>
が送られてきたものとする
節点名
N1
N2
N3
N4
N5
N6
N7
データ名(意味)
A1(会議室=R1)
A2(会議室=R2)
A3(時刻=10時)
A4(時刻=13時)
D2(場所)
D1(時刻)
E(会議)
ラベル
正当化
{{A1}}
{}
{{A2}}
{}
{{A3}}
{}
{{A4}}
{}
{{A1}, (A2)}
{(N1), (N2)}
{{A3}, (A4)}
{(N3), (N4)}
{{A3, A1}, {A3, A2}, {A4, A1}, {A4, A2}}
{(N5, N6)}
①推論システムが「A1とA2が両立しない」及び「A3とA4」が両立しない」ことを伝えると、
②ATMSは、{A1,A2}及び{A3,A4}をNOGOODというデータベースに蓄積する。
③推論システムが「10時に会議室R1が使えない」ことを伝えると、
④ATMSは、{A1,A3}をNOGOODというデータベースに蓄積するとともに、N7から{A3, A1}を削除。
⑤推論システムが「会議室R2が使えない」ことを伝えると、
⑥ATMSは、{A2}をNOGOODというデータベースに蓄積するとともに、A2を含むラベルを削除。
節点名
N5
N6
N7
削除される
ラベル
データ名(意味)
D2(場所)
D1(時刻)
E(会議)
ラベル
{{A1}}
{{A3}, (A4)}
{{A4, A1}}
正当化
{(N1)}
{(N3), (N4)}
{(N5, N6)}
{A1, A2, A3, A4}
{A1, A2, A3}
{A1, A2}
{A1, A2, A4}
{A1, A3}
{A1}
{A1, A3, A4}
{A1, A4}
{A2, A3}
{A2}
{A3}
{}
{A2, A3, A4}
{A2, A4}
{A4}
{A3, A4}