第8章分解証明系 - 講義ノート

θ=[f(x)/x,g(z,b)/y]
σ=[f(z)/x,a/z]
h(x,y,z)θσ=h(f(x),g(z,b),z)σ=h(f(f(z)),g(a,b),a)
こんな代入になるような代入の合成を定義する。

代入θ=[s1/u1, ... , sm/um],σ=[t1/v1, ... ,tn/vn]に対してその合成は
θσ=[s1σ/u1, ... ,smσ/um,t1/v1, ... ,tn/vn]からui=siσとなるようなsiσ/uiと、いずれかのuに等しいvjを取り除いた集合である。

代入の合成に関しては以下の式が成り立つ

代入θ、σに対してσ=θγとなるようなγが存在するなら、θはγより一般的であるという。
（無駄な代入をしないってことかな？）

単純式*1の多重集合であるSに対してある代入θを施したとき、Sの要素が全て同じ単純式となるならば、そのθは単一化子と呼ぶ。θのうちで最も一般的なものを最汎単一化子という。

（証明は難しいので略）
プリント参照。さして難しくないようだ。

*1:項および原子論理式