A Machine-Oriented Logic Based on the Resolution

A Machine-Oriented Logic
Based on the Resolution Principle
導出原理に基づく機械指向論理
G99P0036 圷 弘明
1.概要
導出原理とは
Pが真であるか、またはQが真である
Pが偽であるか、またはRが真である
この二つがわかっているときに
Qが真であるか、またはRが真である
を結論付けることができる
2.予備公式
論文内で使われている基礎的な
文法や意味論
変数・関数記号・述語記号
変数
u,v,w,x,y,z,u1,u2,u3,...
関数記号
a,b,c,d,e,f,g,h,k,a1,b1,… (引数の数を右肩に)
引数の数が0のものを独立定数とする
述語記号
P,Q,R,P1,Q1,… (引数の数を右肩に)
否定 ~
項・原子式・リテラル
項
例:f(x,y) a など
変数
関数記号と、その項の列もまた項である
原子式
例: P(f(x,y),a)
述語記号と、その項の列
リテラル 例:~P(f(x,y),a)
原子式
Aが原子式なら~Aはリテラル
補・節
補
Aが原子式で、Aと~Aの二つのリテラルのお互
いをComplementという
節
リテラルの有限集合(空でも良い)は節である。
空の節は□と書く
例:{~P(f(x,y),a),Q(b)}
基底リテラル・基底節・整型式
基底リテラル
変数を含まないリテラル
P(f(a),g(b))など
基底節
変数を含まない節
{P(f(a)), Q(b)}など
整型式
項とリテラルのみ
エルブラン領域
エルブラン領域
S:任意の節集合
F:Sの中に現れるすべての関数記号
H0=Φ (Fに定数がない場合はH0=a)
Hi+1=Hi∪F(Hi)
H∞:エルブラン領域
例
{{P(x)},{~P(y)}} ⇒ H∞={a}
{{P(b)},{Q(f(x))}} ⇒ H∞={b,f(b),f(f(b)),…}
飽和(Saturation)
飽和(Saturation)
S:任意の節の集合 P:任意の項集合
Sの中から(変数をPの元で書き換えることに
よって)得られるすべての基底節をP(S)であらわ
す。
ひとつの節にある同じ変数は、同じ項で置き換
えられる。
例
S={R(g(b)),S(y)},{Q(f(x))} P={f(a),c}
P(S)={R(g(b)),S(c)},{R(g(B)),S(f(a))},
モデル
基底リテラルの集合で、Complementsなリテ
ラルを含まないものをモデルという。
M:モデル S:基底節の集合
Sのなかのすべての節がMの要素を含む場合、
MはSのモデルである。
一般的には
S:任意の節集合 H:Sのエルブラン領域
Mは「MがH(S)のモデルであるときだけ」Sのモ
デルであるという。
充足可能性
節集合Sは、そのモデルが存在するとき、充
足可能である。また存在しない場合は充足不
能である。
この定義より
空節を含む節集合は充足不能である
節に最低ひとつの要素が必要であるから
空な節集合は充足可能である
モデルはφ
基底融合節(Ground Resolvents)
C,D : 基底節
L⊆C、M⊆Dの単集合L,Mにおいて、それぞれ
の要素がComplementsな関係であるとき、
(C‐L)∪(D-M)はCとDの基底融合節
R:CとDの基底融合節
{C、D}のモデルは{C、D、R}のモデルである。
2つの基底節は有限の基底融合節を持つ
基底融合(ground resolution)
S:任意の基底節の集合
すべてのSの二組の基底融合節とSの要素で成
り立っている基底節の集合をR(S)であらわし、そ
れをSの基底融合という。
N階基底融合(N-th ground resolution)
N回基底融合を繰り返したものをN階基底融合
という。
3.Saturation Procedures
エルブランの定理による推論
エルブランの定理
エルブランの定理
S=有限節集合
P⊆H (H:Sのエルブラン領域)
P(S)が充足不能
上の場合に限ってSが充足不能
Saturation procedure
Saturation procedure
S=有限節集合
P0,P1,P2…⊆H (H:Sのエルブラン領域)
Pj⊆Pj+1 (j≧0)
P0∪P1∪P2…=H
P0(S),P1(s),P2(s)…と順々に調べていく
Level-satulation
エルブラン領域Hにおけるレベル
H0,H1,H2,H3…
H0=Hのすべての独立定数
Hn+1=Hn∪引数がHnに含まれるHの項
この方法だとHnのサイズがすぐ莫大になってし
まう
Level-satulation2
注目すべき点
充足不能なSにおいて適度に小さい次のような
Pが存在する。
P(S)は充足不能
Q⊆Pなら、Q(S)は充足する(最小である)。
このようなPをSのproof setという
4.導出定理と基礎補題
エルブランの定理の拡張とその証明
導出の手順
基本操作
S=基底節
S,R(S),R2(S),…
以下が成立するまで繰り返す
□∈ Rn(S)が成立する
充足不能
Rn(S)=Rn+1(S)となる
充足可能
このいずれかの条件が必ず成立する
• 形成可能な節は有限である
基底導出定理
S=任意の有限の基底節集合
Sが充足不能
⇔ □∈Rn(S)のnが存在する
証明
□∈Rn(S) ⇒ Sが充足不能
自明
Sが充足不能 ⇒ □∈Rn(S)
T=Rn(S)=Rn+1(s) -(終了セット)
Tは基底融合において閉じている
~(□∈T) ⇒ Tは充足可能
(⇒ S(⊆T)は充足可能) を証明すればよい
証明つづき
L1,L2,L3,…,Lk
Tに現れる原子式とリテラルから~を除いたもの
(例) T = { {P},{P,~Q},{Q} } ⇒ L1=P, L2=Q
モデルM
M0=□
Mj=Mj-1∪{Lj} (0<j≦k)
Tのある節の要素が全てMjの要素のComplimentsで
あるときは Mj=Mj-1∪{~Lj}
Mk=Mとする
証明つづき2
次に、¬(T∈□) ⇒ MはSを充足
を背理法で証明する。
Tのある節の要素が全てMiの要素の
Complimentsであるような最小のiをjとし、その節
をCとする。
Mの定義よりMj=Mj-1∪{~Lj}で、CはLjを含む。
要素が全てMj-1∪{Lj}の要素のComplimentsで
ある節Dが存在し、Dは~Ljを含む。
要素が全てMj-1の要素のComplimentsである節
B=(C-{Lj})∪(D-{~Lj})はjの最小性に反する。
エルブランの定理の拡張
エルブランの定理
S=有限節集合
P⊆H (H:Sのエルブラン領域)
P(S)が充足不能⇔Sが充足不能
拡張されたエルブランの定理
S=有限節集合
P⊆H(H:Sのエルブラン領域)
□∈Rn(P(S)) ⇔ Sは充足不能
導出定理の一般化
今までは基底節だけを扱っていた
一般の変数を含む節も扱えるようにする
Rn(S)の一般化
R(S):Sが基底節⇒以前の定義と同じ
明確な定義は後ほど
補題
補題
S:任意の節集合
P:エルブラン領域の部分集合
このとき R(P(S)) ⊆ P(R(S)) が成立
証明は後ほど
補題の系
系
Rn(P(S)) ⊆ P(Rn(S))
証明
n=0のとき、 P(S) ⊆ P(S) で成立
n≦jで系が成立する場合、
Rn+1(P(s))=R(Rn(P(s)))
⊆R(P(Rn(S)))
⊆P(R(Rn(s)))
=P(Rn+1(S))
エルブランの定理のさらなる拡張
補題の系より
S:有限節集合
P⊆H(H:Sのエルブラン領域)
□∈ P(Rn(S)) ⇔ Sは充足不能
変数の項による置き換えでは、空でない節か
ら□を作ることができない。
□∈P(Rn(S)) ⇔ □∈Rn(S)
一般導出定理(エルブラン定理4)
導出定理
S:有限節集合
□∈ Rn(S) ⇔ Sは充足不能
これによって、proof setを知らなくてもRn(S)
までを計算することにより□を導き出せる。
5.代入・単一化・融合
補題を証明するにあたって必要な
定義と理論
代入
代入の構成要素
T/V
Vは変数でTはV以外の項
代入
代入の構成要素の有限集合
同じ変数を含んではならない
項集合P⊇代入θのすべての構成要素の項
θをSubstitution over Pという
空な代入は下段にεが入る
例示化(Instantiation)
任意の代入θを任意の有限記号列Eに例示
化する
Eに出現する変数を対応する項に書き換える
Eθと書く
EθはEのθによる代入例という
有限記号列の集合Cのθによる代入例はCθで、
Cのそれぞれの要素をθで例示化したもの
標準化
C:任意の有限記号列E
V1,V2,V3…Vk : Cに現れる変数
x-標準化
代入 ξc={x1/V1,…,xk/Vk}
y-標準化
代入 ηc={y1/V1,…,yk/Vk}
代入の合成
θ’∪λ’=θλ(合成という)
θ={T1/V1,…,Tk/Vk}とλは任意の代入
λ’の変数はθの変数以外のλの変数を含む
θ’はTiλ/Vi(1≦i≦k)
例
θ={G(x,y)/w,H/z}, λ={A/x,B/y,C/z}
λ’={A/x,B/y}, θ’={G(A,B)/w,H/z}
θλ= {A/x,B/y, H/z ,G(A,B)/w}
代入の合成2
εθ=θε=θ (単位元)
代入の合成の定義より自明
(θλ)μ= θ(λμ) (結合法則)
これにより括弧を省略できる
ポイント
δ= θλなら
E δ = Eθλ (= (Eθ)λ )
代入の合成における諸定理
(Eσ)λ=E(σλ)
∀E(Eσ= Eλ) ⇒ σ= λ
(σλ)μ= σ(λμ)
∀A,B ((A∪B)λ=(Aλ∪Bλ))
不適合な集合
A:任意の整型式の集合
B:Aの不適合な集合
Aのそれぞれの要素(整型式)からその引数の
順番で早いものをとってきた集合
ただし、 Bが全て同じ要素になるときは、その次に順
序的に早いものをとる
例
A={P(x,h(x,y),y),P(x,k(y),y),P(x,a,b)}
B={h(x,y),k(y),a}
単一化
A:任意の整型式の集合
θ:代入
Aθが単集合⇒θはAの単一化代入という
単一化代入が存在するようなAを
単一化可能という
Aが単一化可能で単集合でないとき、Aの不適合
な集合は単一化可能である
単一化のアルゴリズム
単一化アルゴリズム
①σ0=ε, k=0, goto②
②IF(|Aσk| = 1) return Aσ ELSE goto③
③ Aσkの不適合集合のLexical orderで1番目
のをVk,二番目をUkとしたとき、
Vkが変数で、 Ukのなかに現れない場合
• σk+1=σk{Uk/Vk}, k++, goto②
そうでないときは停止
単一化アルゴリズムの正当性
解の正当性
②で停止する場合、解は正しい
③で停止する場合、 Vkが変数でない場合、
Ukのなかに現れる場合ともに単一化不可能
停止性
Aは有限集合なので変数が有限個しかない
AσkはVkを含むが、 Aσk+1は含まない
よって手順③が無限に繰り返されることは
ないので停止する。
再汎単一化代入
Aが②で停止する場合、その返り値が再汎単
一化代入である。
Aは再汎単一化可能といわれる
Key triples
<L,M,N>:リテラルの集合3つ
<C,D>:節のペア
<L,M,N>は<C,D>のKey triplesである
L,M≠φ L⊆C,M⊆D
Nは(LξC)∪(MηD)中の原始式 (~をとる)
NはσNで再汎単一化可能である
(LξC)σN と (MηD)σNはお互いが補であるよう
な要素をもつ単集合である
<C,D>のKey triplesは有限個しかない。
融合節(一般)
節C,Dの融合節
<L,M,N>は<C,D>のKey triplesとする
((C-L)ξCσN) ∪ ((D-M) ηDσN)
のどの節も融合節である
Key triplesの定義より、節C,Dの融合節の個
数は有限である。
この融合節の定義から前回同様にRn(S)が
定義できる。(一般的な)
単一化定理
A:空でない整形式の有限集合
Aが単一化可能 ⇒ AはσAで再汎単一化可能
さらに、任意の単一化代入θで
θ=σAλ
を満たすλが存在する。
証明
前者の定理
単一化アルゴリズムの正当性より自明
後者の定理
任意の単一化代入θにおいて、単一化アルゴリ
ズムのステップkで
θ=σkλk
を満たすλkを考える。
σ0=ε,λ0=θ
証明つづき
k≧1の場合
|Aσk|=1
σkは再汎単一化代入であるから、λ=λkである
|Aσk|≠1
θ=σkλk と仮定する。
η=λk - {Vkλk/Vk}とおくと、
λk={Uk/Vk}ηとなるので、(論文参照)
σkλk =σk {Uk/Vk}η=σk+1η
より、ηが求めたいλk+1である。
補題の証明
補題
S:任意の節集合
P:Sのエルブラン領域の部分集合
このとき R(P(S)) ⊆ P(R(S)) が成立
証明
A ∈ R(P(S))を仮定
A∈P(S) ⇒ S⊆R(S) ⇒ A∈P(R(S))
¬(A∈P(S)) ⇒ Aは融合節
証明つづき
AはCα,Dβの融合節
C,D∈S
α={T1/V1,T2/V2,…,Tk/Vk}
(V1~Vk:Cの変数全て, T1~Tk∈P)
β={U1/W1,U2/W2,…,Uk/Wk}
(W1~Wk:Dの変数全て, U1~Uk∈P)
L⊆C,M⊆D
(L,M≠φでLα,Mβは互いに補な単集合)
A=(C - L)α∪(D - M)β
証明つづき2
θ={T1/x1,…,Tk/xk, U1/y1,…,Um/ym}
A= (C - L)ξCθ∪(D - M)ηDθ
• 書き方が変わっただけ → Lα=LξCθ , Mβ=MηDθ
N: (LξC)∪(MηD) に発生する原始式の集合
• リテラルから否定記号を除いたものも含む
θはNを単一化する
θ=σNλ (単一化定理より)
証明つづき3
B = ((C-L)ξCσN) ∪ ((D-M) ηDσN)
<L,M,N>は<C,D>のKey triplesである
融合節BはSに属する
B∈R(S)
A=Bλ なので A∈P(R(S))
※Lemmaの逆は成立しない
//
ろん
ばく
6.論駁
導出定理を使って実際に証明をする
論駁
我々の使う唯一の推論規則
二つの節から新しい節を融合する
Sの論駁とは
B1,B2,B3,…,Bn は節で、どちらかを満たす
Bi∈S
Bi:融合された節
Bnは□である。
Sの論駁が存在する⇔Sが充足不能
導出定理より
実際の論駁例
次の節を含む集合S
C1={Q(x, g(x), y, h(x,y), z, k(x,y,z))}
C2={~Q(u, v, e(v), w, f(v,w), x)}
Sの要素が二つなので、key tripleは自動的
に決定する
<C1,C2,N>
N : { Q(x1,g(x1),x2,h(x1,x2),x3,k(x1,x2,x3))
Q(y1,y2,e(y2),y3,f(y2,y3),y4) }
実際の論駁例(2)
単一化アルゴリズムを実行し、σNを求める
σN = { y1/x1 , g(y1)/y2 , e(g(y1))/x2 ,
h(y1,e(g(y1)))/y2 ,
f(g(y1),h(y1,e(g(y1))))/x3
, k(y1,e(g(y1)),f(g(y1),h(y1,e(g(y1)))))/y4 }
融合節は□である。
level-satuationでは事実上証明不可能
エルブラン領域が広すぎる(level5で10^256)
7.Search Principle
効率よく論駁するための方法
論駁の停止性
S:以下の節の集合
C1 : {Q(a)} , C2 : {~Q(x),Q(f(x))}
このSは永遠に融合節を作りつづける
{Q(f(a))}, {Q(f(f(a)))}, {Q(f(f(f(a))))}, …
Sは自然数の定義である
純リテラル(Pure Literals)
S:任意の有限節集合
L:L∈C∈S
LがSで純リテラルであるとは
任意の節ペア<C,D>においてkey triple
<{L},M,N>が存在しない
D∈Sー{C}
Purity theorem
Purity theorem
S:任意の有限節集合
L:L∈C∈S で、純リテラルである
Sは充足可能 ⇔ S - {C}が充足可能
Purity theoremの例
Purity theoremによって、純リテラルを含む節
を削除できる。
例
C1 : {Q(a)} , C2 : {~Q(x),Q(f(x))}
C2のQ(f(x))は純リテラルなので除去できる
C1 : {Q(a)}
C1のQ(a)は純リテラルなので除去できる
S=□ ⇒ Sは充足可能
Subsumption
C,D:空でない異なる節
∃σ(Cσ⊆D) ⇒ CはDを包括する
Subsumption定理
S: 任意の有限節集合
D: D∈S E: E∈(S - {D})
Dを包括するEが存在する
Sが充足可能 ⇔ S - {D}が充足可能
Subsumptionアルゴリズム
 ① V1,V2,…Vm : D中の異なる全ての変数(アルファベット順)
J1,J2,…Jm : C,Dに含まれない互いに異なる定数
θ={J1/V1, J2/V2, … , Jm/Vm}
Dθを計算して②へ
 ② A0={C}, k=0, ③へ
 ③ Akが□を含まない ⇒
K∈Ak, M⊆K, N=M∪{P}, P∈Dθ, NはσNで再汎単一化可能
Ak+1=(KσN - MσN)の集合
④へ
Akが□を含む ⇒ 停止
 ④ Ak+1≠φ ⇒ k++, ③へ
Ak+1=φ ⇒ 停止