有限項に対する(一階の)単一化アルゴリズムは推論規則を用いて形式化され,その停止性,健全性と完全性が多くの文献で示されている.また,いくつかの先行研究において,正則項に対する単一化アルゴリズムも推論規則を用いて与えられている.しかしながら,それらの研究において,与えられた等式集合から推論規則により得られた集合の解ともとの集合の最汎単一化子である正則代入が一致することは明確に示されていない.また,停止性,健全性と完全性の明確な証明を与えているものはない.本論文では,正則項に対する単一化アルゴリズムの基礎理論を項書換えシステムの枠組みで整理し直すことを目標とする.まず,再帰式表現の解はその再帰式表現に対応する等式集合の最汎単一化子であることを示す.次に,正則項に対する単一化アルゴリズムを推論規則を用いて再定式化し,その停止性,健全性と完全性の明確な証明を示す.最後に,単一化可能な等式集合は正則代入で表現される最汎単一化子をもつことの完全な証明を与える.