x - 京都大学

知能情報システム特論
証明と所属性判定(2)
山本章博
京都大学情報学研究科知能情報学専攻
http://www.iip.ist.i.kyoto-u.ac.jp/member/akihiro/
[email protected]
目標
基礎原子論理式の集合(Herbrand base) Bの部
分集合) を論理式 F を用いて
S = {p(t1, t2,…,tn) | F |= p(t1, t2,…,tn) }
と定義したとき，
基礎原子論理式 p(s1, s2,…,sn) について
p(s1, s2,…,sn)  S
であるかどうかを判定する手続きを与える

論理的帰結と集合(2)
例
j1 = even(0)
j2 = "x (even(s(x))  even(x))
Seven = { even(t) | j1, j2 |= even(t) }
even(0) Seven,
even(s(s(0))) Seven ,
even(s(0)) Seven ,
even(s(s(s(0))))Seven ,
...
論理的帰結と集合(3)
例 j1 = "x plus (0, y, y)
j2 =
"x "y "z plus(s(x),y,s(z))  plus(s(x),y,s(z))
Splus ={plus (t, s, u) | j1 , j2 |= plus (t, s, u) }
plus(0, s(0), s(0))  Splus,
plus(s(0), s(0), s(s(0)))  Splus,
plus(s(0), 0, s(s(0))) Sgeq, ...
形式的な証明
意味論と証明論(1)



論理式の“正しさ”の形式化に対する二つの立場
意味論：論理式の表す内容を形式化
命題の正しさを0, 1で表現
論理演算子の意味をBoole演算で表現
証明論：演繹的な推論を論理式の操作として形
式化
論理演算子の使い方を推論規則で表現
意味論と証明論(2)

意味論による“正しさ”




証明論による“正しさ”



解釈 I : 命題変数へ0, 1を代入
恒真式：任意の解釈 I について I(j) = 1である j
論理的帰結 j1, ... , jn |= z ：
I(j1 ) =…= I(jn ) = 1 である任意の解釈 I に
対して I(z ) = 1
j1, ... , jn |- z ：j1, ... , jn を仮定して z が導出される
定理式： |- j である j
健全性 j1, ... , jn |- z ならば j1, ... , jn |= z
完全性 j1, ... , jn |= z ならば j1, ... , jn |- z
“ならば”, “ならば”, “ならば”
j  z : 論理演算子としての“ならば”
j |= z : 意味上の帰結としての“ならば”
j |- z : 演繹推論操作としての“ならば”


演繹定理
j1, ... , jn |= z と |= j1  ... jn  z は同値
に対する推論規則
[j ]
j
jz
…
z
z
jz
演繹における命題，証明

命題：正しさを考察対象とする文


数学では，その意義や用途に応じて，定理，補題，
命題，公理，などと呼ばれる
証明：命題から命題を次々と導く連鎖
証明の例
考察の対象：ユークリッド幾何
定理三角形ABCが二等辺ならば底角は等しい
A B = A C ABC = ACB
A
B
C
明示的には用いていない命題
A



AB=AC (1)  AC=AB (2)
BAC = CAB (3)
三角形の合同条件


B
二辺とその挟角が等しい三角形は合同
DBAC  DCAB (4)  ABC= ACB (5)

合同な三角形の角が等しい
C
公理

公理：証明なしで正しさを認める命題
証明の始点


証明：命題から命題を次々と導く連鎖Þ始点が必要
公理の設定が考察対象領域を決めてしまう．
例前出の証明で用いる公理
 等号の対称性: AB=AC  AC=AB
 角の対称性: BAC=CAB
 合同: AB=EF AC=EG BAC=FEG  DABCDEFG
 合同な三角形の角が等しい:
DBAC  DCAB  ABC= ACB
証明の構造(2)
AB=AC
BAC = CAB
AB=AC  AC=AB
AC=AB
AB=AC
BAC = CAB  AC=AB  AB=AC
(BAC CAB  AC=AB  AB=AC) DBAC  DCAB
DBAC  DCAB  ABC= ACB DBAC  DCAB
ABC = ACB
命題の構造と証明(1)
AB=AC
BAC = CAB
AB=AC  AC=AB
AC=AB
AB=AC
BAC =CAB  AC=AB  AB=AC
(BAC  CAB  AC=AB  AB=AC)DBAC  DCAB
DBAC  DCAB  ABC= ACB DBAC  DCAB
ABC = ACB
命題の構造と証明(2)
B=C
BC=CB
BC=CB
B=C  C=B
C=B
B=C
 C=B  B=C
BC=CB  C=B  B=C
DBAC  DCAB 
AB=AC
 DBAC  DCAB
DBAC  DCAB
AB=AC
命題の構造と証明(3)
p

p
r
q
r

q
p

r
s

q
p
q
p
t

s
t
s
命題の構造と証明(4)



証明は命題中に用いられている論理結合子
 (ならば)
 (かつ)
の用法に従って構成されている．
用法と構成の関係は，命題が何を表している
かには依存しない．
表記法
j
q
j
q
d
d
j
q
d
融合原理(命題論理の場合)
恒真式,恒偽式

恒真式: どのような解釈 I に対しても I (j ) = 1
例
even(s(s(0))   even(s(s(0))
"x "y (= (d(x, y), d(y, x)))
 $x $y ((= (d(x, y), d(y, x))))

恒偽式: どのような解釈 I に対しても I (j ) = 0
例
"x (even(s(s(x))))  " x
(even(s(s(x))))
CNF(1)
リテラル(literal)：命題変数一つからなる式 p
命題変数にを用いた式  p
 節(clause)：有限個のリテラルを  でつないだ式
p1p2 … q1q2...
p1, p2 , …q1 , q2, ...
 CNF: 有限個の節を  でつないだ式
例 (p  q)  (p  q)  ( p  q)  ( p   q)

(p  q)  (p, q )  (q  p )  ( p, q)
pq
CNF(2)


論理式 j に対して
任意の解釈 I について I(j) = I(z )
CNF z が存在する.
以後しばしば, CNFを
C1  C2  …  Cn (Ci は節)
Ci = A1, A2 , …B1 , B2, ...
とかく
節論理


演繹定理
j1, ... , jn |= z と |= j1  ... jn  z は同値
特に CNF C1  C2  …  Cn に対して
C1, ... , Cn |= z と |= C1  ... Cn  z は同値
z として節だけを考えれば,
論理式として節だけを用いる体系
ができる

数式で1次式だけを用いる体系（線形代数）を考え
ることに対応
例
命題変数 p : AB=AC , q : AC=AB
r : BAC = CAB,
t : △ABC  △ ACB,
s : ∠ABC =∠ACB,
p
qp
r
t  p, q, r
B
st
A
C
節に対する推論規則(1)

節は論理演算子の出現方法が限定されている
ため, 操作方法も限定することが可能
Resolution(融合, 導出)
p, p2 ,…, q1, q2 ,…,r1, r2 ..., s1, s2 ...は命題変数
pp2 …q1q2...
r1 r2...ps2...
p2... r1 r2… q1 q2... s2...
p, p2 , … q1, q2,...
r1, r2, ... p, s2,...
p2,..., r1, r2,…q1, q2,...,s2,...
節に対する推論規則(2)
…Li…Lk … (Li, Lkはリテラル)
…Lk…Li …
…Li…Lk …
…Li…
…
Subsumption(包摂)
…Li… …
…Li…Lk …
(Li, Lkはリテラル, Li = Lk)
(Li, Lkはリテラル)
例(1)
p : AB=AC , q : AC=AB , r : BAC = CAB,
t : △ABC  △ACB, s : ∠ABC =∠ACB
t  p, q, r
p
qp p
t  q, r
q
tr
r
t
st
s
B
A
C
例(3)
p : AB=AC , q : AC=AB , r : BAC = CAB,
t : △ABC  △ ACB, s :∠ABC =∠ACB
s st
t
t  p, q, r
 p, q, r
p
 q, r
qp
 p,r
p
r
r
 (q)
A
B
C
融合原理の演繹完全性[Lee]
CNF C1  C2  …, 節 p1, p2, …q1, q2,...
C1  C2  … |= p1, p2, …q1, q2,...

pi = qk なる i, k が存在するか, または,
C1 , C2 ,…, から融合によって導出できる節 Dで
p1, p2, …q1, q2,... を包摂するものが存在する
j1, ... , jn |- z ならば j1, ... , jn |= z
融合原理の反駁完全性[Robinson]
CNF C1  C2  … が恒偽
 C1 , C2 , … から融合によって空節が導出でき
る．
CNF C1  C2  …, 節 p1, p2, …q1, q2,...
C1 , C2 , … |= p1, p2, …q1, q2,...
 C1 , C2 , … ,  p1,  p2, … , q1 , q2 ,...
から融合によって空節が導出できる．
融合原理(述語論理の場合)
述語論理の論理式



命題定数： ^ (□), T (■)
原子論理式 : 定数(対象)記号: 0, A, B,...
関数記号: s, d, ...
述語記号: even, mod, ...
変数(対象変数): x, y, z,…
論理演算子：  (でない),  (かつ),  (または),
 (ならば),  (同値)
量化子：
" (全ての), $ (ある)
以上の構成要素を用いて，数式と同じ要領で
式を構成する. (括弧は適宜省略)
一般性を表す命題の記号化(1)

一般に成立する命題
“一般に自然数 x は 0 以上である”
という場合，特定の数0, 1, 2, …を指していない
geq(0, 0)  geq(s(0),0)  geq(s(s(0)), 0))
geq(s(s(s(0))), 0)  …


数式の P n=1 に相当
“任意の数 x に対して 0 に x を加えた結果は x
である”
"x geq (x, 0)
一般性を表す命題の記号化(2)
例
"x geq (x, 0)
"x "y (geq(s(x), s(y))  geq(x, y))
"x (even(s(s(x))  even(x))
"x plus (0, y, y)
"x "y "z plus (y, x, z)  plus (x, y, z)
"x "y "z plus(s(x),y,s(z))  plus(s(x),y,s(z))
述語論理式の標準形


リテラル(literal)：
原子論理式一つからなる式 A
原子論理式にを用いた式  A
節(clause)
"x1...xk (A1  A2 ... An B1  B2 ... Bm)
x1,...,xk はA1, A2,..., An,B1 , B2 ,..., Bmに現れる変
数全てのリスト
A1, A2,..., An  B1, B2,..., Bm

節形式文: 有限個の節を  でつないだ式
標準形(DNF)



節(clause)または項(term)：
有限個のリテラルを  でつないだ式
p1  p2  …  q1  q2 ...
p1, p2 , …q1 , q2, ...
DNF: 有限個の節を  でつないだ式
Affirmative(DNFの一般化)
節形式文 : 節の選言 C1  C2  …  Cm
節(clause, 単項式 monomial)
$x1... $xk (A1  A2 ...  An  B1  B2 ...  Bm )
全称記号に対する推論規則
"x1"x2 …"xn. j
j [x1 = t1, x2 = t2 ,…, xn = tn ]
例
"x"y"z"u. xy=zu  zu=xy
AB=AC  AC=AB
"x"y "z.  x y z= z y x
BAC=CAB
ti は具体的な対象
注意

命題の一般性の構造は，命題が表現する内
容に依存する．
例

"x"y "z.  x y z= z y x
"x"y. x z= z x
数理論理学では
命題論理: 一般性を扱わない
述語論理: 一般性を扱う
Herbrandの定理
j = "x1 " x2 …" xn y
yには x1, x2,…,xn 以外の変数は現れない
yには全称記号も存在記号も現れない
という形の論理式がどのような解釈に対しても
I(j) = 0 となる

Herbrand空間の基礎項を変数代入して得られ
る有限個の式の連言 yq1  yq2  …  yqm
がどのような解釈に対してもI(j) = 0 となる
例(1-1)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(0) 
even(s(s(0))) 
even(s(s(0)))  even(0)
even(s(s(s(s(0)))))even(s(s(0)))
even(s(s(s(s(0))))) 
例(1-2)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(s(s(s(s(0)))))even(s(s(0)))
even(s(s(0)))even(0)
even(s(s(s(s(0)))))  even(0)
even(0) 
even(s(s(s(s(0))))) 
例(1-3)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(s(s(s(s(0)))))
even(s(s(s(s(0)))))even(s(s(0)))
even(s(s(0)))
even(s(s(0)))  even(0)
even(0)
even(0) 
q
例(2-1)
y))
j1 = "x geq (x, 0) 
j2 = "x "y (geq(s(x), s(y))  geq(x,
j1q1 = geq(s(0), 0) 
j2q2 = geq(s(s(0))), s(0))  geq(s(0), 0)
j2q3 = geq(s(s(s(0))),
s(s(0))) 
geq(s(s(0)),
s(0))
geq(s(0)),
0) 
geq(s(s(0))),
s(0))
 geq(s(0),
0)
geq(s(s(0))), s(0)) 
geq(s(s(s(0))), s(s(0)))  geq(s(s(0)), s(0))
geq(s(s(s(0))),s(s(0))) 
例(2-2)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
geq(s(s(s(0))), s(s(0)))  geq(s(s(0)), s(0))
geq(s(s(0))), s(0))  geq(s(0), 0)
geq(s(s(s(0))), s(s(0)))  geq(s(0), 0)
geq(s(0), 0) 
geq(s(s(s(0))),s(s(0))) 
例(2-3)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
 geq(s(s(s(0))),s(s(0)))
geq(s(s(s(0))), s(s(0)))  geq(s(s(0)), s(0))
 geq(s(s(0))), s(0))
geq(s(s(0))), s(0))  geq(s(0), 0)
 geq(s(0)), 0)
q
 geq(s(0)), 0)
例(3-1)
j1 = "x plus (0, y, y) 
j2 = "x "y "z plus(s(x), y, s(z))plus(x, y, z)
j1q1 = plus(0, s(0), 0) 
j2q2 = plus(s(0), s(0), s(s(0)))  plus(0, s(0), s(0))
plus(0, s(0), s(0)) 
plus(s(0), s(0), s(s(0)))  plus(0, s(0), s(0))
plus(s(0), s(0), s(s(0))) 
例(3-2)
j1 = "x plus (0, y, y) 
j2 = "x "y "z plus(s(x), y, s(z))plus(x, y, z)
 plus(s(0), s(0), s(s(0)))
plus(s(0), s(0), s(s(0)))  plus(0, s(0), s(0))
 plus(0, s(0), s(0))
q
plus(0, s(0), s(0))
述語論理の節形式文の性質

論理式 j に対して
j が恒偽式であるときかつそのときに限り
z が恒偽式である
を満たす節形式文 z が存在する.
(注)
 論理式 j に対して
任意の解釈 I について I(j) = I(z )
なる節形式文 z が存在するとは限らない
節論理


演繹定理
j1, ... , jn |= z と |= j1  ... jn  z は同値
特に節形式 C1  C2  …  Cn に対して
C1, ... , Cn |= z と |= C1  ... Cn  z は同値
z として節だけを考えれば,
論理式として節だけを用いる体系
ができる
標準形と推論規則(1)

Resolution(融合, 導出)
A, A2,…  B1, B2,...
C1, C2,...  D, D2,...
(A2,..., C1, C2,…  B1, B2,..., D2,...)q
q : 単一化代入 (unifier)


下の節をresolvent(導出節, 融合節)とよぶ
因子化(factoring)
A1, A2,..., Ai, Ai +1,…  B1, B2,...
(A, Ai +1,…  B1,B2,...)d
d : 単一化代入 (unifier)
基本的な考え方
CA
AB
C B
の拡張
 命題論理の場合，A, B, Cは命題変数だから,
構文上は「同じ」か「異なる」のいずれか
 述語論理は「変数への代入で一致させる」とい
う可能性がある
CD
AB
(C  B) q
q : Dと Aの単一化代入
代入
q = {x1:= t1,..., xn:= tn }

論理式や項に現れる変数x1 ,..., xnを項t1,...,tnに
同時に置換える操作


同じ変数は同じ項に置換える
何も置換えを行わない代入（空代入） {} または e
例 q = {x := s(0), y := 0}
plus(s(x),y ,s(z))q = plus(s(s(0)),0,s(z))
d = {x := s(y), y := 0}
plus(s(x),y ,s(z))d = plus(s(y), 0 ,s(z))



plus(s(x),y ,s(z))d  plus(s(0), 0 ,s(z))
単一化代入(unifier)
q = {x1:= t1,..., xn:= tn }
複数個の原子論理式や項 A1,..., Amを一致させ
る代入
例 A1 : p(d(x, B), d(A, u))
A2 : p(d(A, B), d(A, C))
q ={x := A, u := C}
例 A1 : plus(0, x, x)
A2 : plus(x’, y’, z’ )
q ={y’ := x, z’ := x }

標準形と推論規則(2)
…Li…Lk … (Li, Lkはリテラル)
…Lk…Li …
…Li…Lk …
…Li…
…
(Li, Lkはリテラル, Li = Lk)
Subsumption(包摂)
…Li… …
…Li…
…
…Li q1Li q2…Li qn… …Li…Lk …
(Li, Lkはリテラル, qは代入)

例(1-1)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(0) 
even(s(s(0))) 
even(s(s(x)))  even(x)
{ x := 0 }
even(s(s(x’ )))  even(x’ )
{ x ’:= s(s(0)) }
even(s(s(s(s(0))))) 
例(1-2)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(s(s(x)))  even(x)
{ x := s(s(x’ )) }
even(s(s(x’ )))  even(x’ )
even(s(s(s(s(x’ )))))  even(x’ )
even(0) 
{ x ’:= 0 }
even(s(s(s(s(0))))) 
例(1-3)
j1 = even(0) 
j2 = "x even(s(s(x)))  even(x)
j2q1 = even(s(s(0)))  even(0)
j2q2 = even(s(s(s(s(0)))))  even(s(s(0)))
even(s(s(s(s(0)))))
even(s(s(x)))  even(x)
{x := s(s(0))}
even(s(s(x’ )))  even(x’ )
even(s(s(0)))
{x’ := 0}
even(0)
e
even(0) 
q
例(2-1)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
j1q1 = geq(s(0), 0) 
j2q2 = geq(s(s(0))), s(0))  geq(s(0), 0)
j2q3 = geq(s(s(s(0))), s(s(0)))  geq(s(s(0)), s(0))
geq(x, 0) 
geq(s(x’ ), s(y’ ))  geq(x’ , y’ )
{x := x’ , y’ := 0 }
geq(s(x), s(0)) 
geq(s(x’’ ), s(y’’ ))  geq(x’’ , y’’ )
{x ’’:= s(x), y ’’ := s(0)}
geq(s(s(x))),s(s(0))) 
例(2-1)





y))
j1 = "x geq (x, 0) 
j2 = "x "y (geq(s(x), s(y))  geq(x,
geq(s(x), s(0)) 
geq(s(s(x)), s(s(0))) 
geq(s(s(s(x))), s(s(s(0)))) 
例(2-1)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
geq(x, 0) 
geq(s(x’ ), s(y’ ))  geq(x’ , y’ )
{x := x’ , y’ := 0 }
geq(s(x), s(0)) 
geq(s(x’’ ), s(y’’ ))  geq(x’’ , y’’ )
{x ’’:= s(x), y ’’ := s(0)}
geq(s(s(x)),s(s(0))) 
{x := s(0)}
geq(s(s(s(0))),s(s(0))) 
例(2-2)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
geq(s(x), s(y))  geq(x, y)
geq(s(x’ ), s(y’ ))  geq(x’ , y’ )
{x := s(x’ ), y :=
s(y’ )}
geq(s(s(x’ )),s(s(y’ )))  geq(x’ , y’ )
geq(x’’, 0)
{y’ := 0 }
geq(s(s(x’’ )),s(s(0))) 
{x’’ :=
s(0)
}
geq(s(s(s(0))),s(s(0)))

例(2-3)
j1 = "x geq (x, 0) 
j2 = "x "y geq(s(x), s(y))  geq(x, y)
 geq(s(s(s(0))),s(s(0)))
geq(s(x), s(y))  geq(x, y)
{x := s(s(0)), y := s(0)}
 geq(s(s(0))), s(0))
geq(s(x’ ), s(y’ ))  geq(x’ , y’ )
 geq(s(0)), 0)
q
{x’ := s(0), y’ := 0}
 geq(x’’ , 0)
{x’’ := s(0)}
例(3-1)
j1 = "x plus (0, y, y) 
j2 = "x "y "z plus(s(x), y, s(z))plus(x, y, z)
j1q1 = plus(0, s(0), 0) 
j2q2 = plus(s(0), s(0), s(s(0)))  plus(0, s(0), s(0))
plus (0, y, y) 
plus(s(x’ ), y’, s(z’ ))plus(x’ , y’, z’ )
{x’ := 0, y’ := y, z’ := y }
plus(s(0), y, s(y)) 
{y := s(0)}
plus(s(0), s(0), s(s(0))) 
例(3-2)
j1 = "x plus (0, y, y) 
j2 = "x "y "z plus(s(x), y, s(z))plus(x, y, z)
 plus(s(0), s(0), s(s(0)))
plus(s(x), y, s(z))plus(x, y, z)
{x := 0, y := s(0), z := s(0)}
 plus(0, s(0), s(0))
q
plus (0, y’ , y’ ) 
{y’ := s(0)}
融合原理の演繹完全性[Lee]
CNF C1  C2  …, 節 p1, p2, …q1, q2,...
C1  C2  … |= p1, p2, …q1, q2,...

pi = qk なる i, k が存在するか, または,
C1 , C2 ,…, から融合によって導出できる節 Dで
p1, p2, …q1, q2,... を包摂するものが存在する
j1, ... , jn |- z ならば j1, ... , jn |= z
融合原理の反駁完全性[Robinson]
CNF C1  C2  … が恒偽
 C1 , C2 , … から融合によって空節が導出でき
る．
CNF C1  C2  …, 節 p1, p2, …q1, q2,...
C1 , C2 , … |= p1, p2, …q1, q2,...
 C1 , C2 , … ,  p1,  p2, … , q1 , q2 ,...
から融合によって空節が導出できる．
単一化代入(unifier)
q = {x1:= t1,..., xn:= tn }
複数個の原子論理式や項 A1,..., Amを一致させ
る代入
例 A1 : p(d(x, B), d(A, u))
A2 : p(d(A, B), d(A, C))
q ={x := A, u := C}
例 A1 : plus(0, y, y)
A2 : plus(x’, y’, z’ )
q ={y’ := y, z’ := y }

単一化代入(unifier)(2)

単一化代入は複数個存在することがある
A1 : plus(0, y, y)
A2 : plus(x’, y’, z’ )
q ={x’ := 0, y’ := y, y’ := y}
d ={x := 0, x’ := 0, y’ := 0, z’ := 0}
s ={x := s(u), x’ := 0, y’ := s(u), z’ := s(u)}
単一化可能性
単一化代入: 複数個の原子論理式や項 t1,..., tn
を一致させる代入 q = {x1:= s1,..., xn:= sn }


t1,..., tn に対する単一化代入が存在するとき，
t1,..., tnは単一化可能であるという
t1,..., tn に対する単一化代入が存在しないとき，
t1,..., tnは単一化不可能であるという
単一化(1)
p(d(x, B), d(A, u)) p(d(A, B), d(A, C))
p(d(x, B), d(A, u)) = p(d(A, B), d(A, C))
d(x, B) = d(A, B)
d(A, u) = d(A, C)
x=A
B=B
x =A
A=A
u =C
u=C
単一化(2)
plus(0, y, y) plus(x’, y’, z’ )
plus(0, y, y) = plus(x’, y’, z’ )
0 = x’
y = y’
y = z’
x’ = 0
y’ = y
z’ = y
連立等式の集合の解形式

次の形の連立等式を解形式(solved form)という
x1 = t1
x2 = t2
...
xn = tn
x1, x2,..., xnは相異なる変数
t1, t2,..., tnはx1, x2,..., xnを含まない項
単一化アルゴリズム(1)

1.
原子論理式または項 A1, A2 に対して A1= A2
からはじめて, 次のいずれかの操作解形式に
なるまで適用する．
先頭の同じ関数記号を消去する．
f (t1, t2,..., tn) = f (s1, s2,..., sn)
t1 = s1
t2 = s2
...
tn = sn
単一化アルゴリズム(2)
2.
3.
同じ定数記号または変数からなる等式を消去
する．
a=a
または
x=x
t = x (t は変数ではない項, xは変数)という形
の等式の左辺と右辺を入れ替える
t=x
x=t
単一化アルゴリズム(3)
4.
x = t (t は変数ではない項, xは変数)という形
の等式がある変数 x が他の等式に表れてい
れば, 他の等式中の x に t を代入する
x=t
x=t
t1 = s1
t1q = s1q
q = {x:= t}
...
tn = sn
tnq = snq
単一化アルゴリズム(4)
4.

両辺の先頭が異なる関数記号または定数記
号である等式があれば， “単一化不可能”を
出力して停止する
f (t1, t2,..., tn) = g (s1, s2,..., sm)
または f (t1, t2,..., tn) = a
または a = f (t1, t2,..., tn)
または a = b
左辺が変数 x，右辺は変数ではない項であり
しかも x を含むような等式があれば， “単一
化不可能”を出力して停止する
x = t[x]
代入の合成(1)
q = {x1:= t1,..., xn:= tn }の d = {y1:= s1,...,ym:= xm }の
合成qd :
{x1:= t1d,..., xn:= tnd , y1:= s1,..., yn:= sn }
から xi = yj であるような yj:= sj を除く
例 q = {x’ := x, y’ := B, z’ :=z}, d = {x := A, z’ =
C}
qd = {x’ := A, y’ := B, z’ :=z, x := A, z ’= C}
例 q = {x’ := s(x), z’ := s(z)},
d = {x :=0, z := s(0)}
qd = {x’ := s(0), z’ :=s(s(0)), x :=0, z := s(0)}}
代入の合成(2)
命題原子論理式または項 t と代入 q, d に対して
(t q)d = t (qd)
例q = {x’ := x, y’ := B, z’ :=z }, d = {x := A, z’ = C}
qd = {x’ := A, y’ := B, z’ :=z, x := A, z ’= C}
p(x’, y’, z’ )q = p(x, B, z)
(p(x’, y’, z’ )q)d = p(A, B, z)
p(x’, y’, z’ )qd = p(A, B, z)
代入の合成(3)
例 q = {x’ := s(x), z’ := s(z)},
d = {x :=0, z := s(0)}
qd = {x’ := s(0), z’ :=s(s(0)), x :=0, z := s(0)}}
plus(x ’, y ’, z ’)q = plus(s(x), y ’, s(z))
(plus(x ’, y ’, z ’)q)d = plus(s(0), y ’, s(z))
plus(x ’, y ’, z ’)(qd) = plus(s(0), y ’, s(s(0)))
最汎単一化代入(mgu)

原子論理式や項 A1,..., Amの単一化代入qで
他のどのような単一化d に対しても
d = qs
であるような代入sが存在するとき, q を最汎単
一化代入(most general unifier, mgu)という
例 A1 : plus(0, y, y) A2 : plus(x’, y’, z’ )
q ={x’ := 0, y’ := y, z’ := y }
d ={ x := 0, x’ := 0, y’ := 0, z’ := 0}
s ={x := s(u), x’ := 0, y’ := s(u), z’ := s(u)}
単一化アルゴリズムの正当性
定理原子論理式または項 A1= A2に対して, 単
一化アルゴリズムを適用すれば,有限時間内
に停止して,

A1 と A2 が単一化可能であれば，それらの最
汎単一化代入(mgu)が出力される

A1 と A2 が単一化可能でなければ，“単一化
不可能”を出力して停止する

Download Report