ユニフィケーション
この形式の多重集合は置換を表しているとみなすことができる。解がない場合、アルゴリズムは ⊥ {\displaystyle \bot } とともに停止する。項 t {\displaystyle t} に含まれる変数群を V a r s ( t ) {\displaystyle Vars(t)} と表記し、問題 G {\displaystyle G} 内の式の左辺と右辺の全ての項に含まれる変数の集合は V a r s ( G ) {\displaystyle Vars(G)} と表記する。問題 G {\displaystyle G} 内での変数 x {\displaystyle x} の出現を全て項 t {\displaystyle t} に置換することを G { x ↦ t } {\displaystyle G\{x\mapsto t\}} と表記する。簡単にするため、定数記号は引数ゼロ個の関数記号とみなす。
G ∪ { t = ? t } ⇒ G {\displaystyle G\cup \{t{\stackrel {\text{?}}{=}}t\}\Rightarrow G}
G ∪ { f ( s 1 , ... , s k ) = ? f ( t 1 , ... , t k ) } ⇒ G ∪ { s 1 = ?
, s k ) } {\displaystyle G\cup \{f(s_{1},\dots ,s_{k}){\stackrel {\text{?}}{=}}x\}\Rightarrow G\cup \{x{\stackrel {\text{?}}{=}}f(s_{1},\dots ,s_{k})\}}
G ∪ { x = ? t } ⇒ G { x ↦ t } ∪ { x = ? t } if x ∈ V a r s ( G ) ∧ x ∉ V a r s ( t ) {\displaystyle G\cup \{x{\stackrel {\text{?}}{=}}t\}\Rightarrow G\{x\mapsto t\}\cup \{x{\stackrel {\text{?}}{=}}t\}{\text{ if }}x\in Vars(G)\land x\notin Vars(t)}
G ∪ { x = ? f ( s 1 , ... , s k ) } ⇒ ⊥ if x ∈ V a r s ( f ( s 1 , ... , s k ) ) {\displaystyle G\cup \{x{\stackrel {\text{?}}{=}}f(s_{1},\dots ,s_{k})\}\Rightarrow \bot {\text{ if }}x\in Vars(f(s_{1},\dots ,s_{k}))}