りったんの学士論文

単一化アルゴリズム(unification algorithm)

[定理] 単一化アルゴリズムの停止性単一化可能な基本論理式の有限集合 W (≠φ)が与えられたとき，上で示した単一化アルゴリズムはステップi+1(有限回)で停止し，そのとき(a)で停止すれば得られたθ_i は最汎単一子である．

{A₁, A₂, ..., A_n} を調べようとする基本論理式の集合であるとする．

[ステップ0] 空な代入θ₀ (つまり何もしない)から出発する．

[ステップi+1] ステップi(i ≧0) で得られた代入をθ_i とする．

(a) 代入を受けた集合{A₁θ_i, A₂θ _i, ..., A_nθ_i} がすべて同じになるとき，このθ_iを最汎単一子(mgu)という．この場合のA₁θ _i を因子(factor)とよぶ．そしてアルゴリズムは終了する．

(b) そうでなければ，

{A₁θ_i, A₂θ _i, ..., A_nθ_i}

の不一致集合を求めて，これを D_i とする．D_i の中に固体変項 v_i と項 t_i があり，t_i の中に v_i が現れないとすれば(この検査を「出現検査」(occur check)という)，これを t_i/v_iという代入とし，θ _i に加えて

θ_i+1 = θ_i○{t_i/v_i}

を作る．すなわち，θ_i の中に現れる全ての v_i を t_i に置き換え，t_i/v_i を加える．このような v_i，t_i が存在しなければ，これらの基本論理式の間には単一子はないとしてアルゴリズムは終了する．

(例)
W = {P(a, x, f(x)), P(y, g(y), z)} の最汎単一子を求めよ．最汎単一子が存在する場合は，因子も求めよ．