1階述語論理の推論。ユニフィケーションアルゴリズム。2つの式を比較し、変数に割り当てを行う。ユニフィケーションの和訳は単一化。
"Artificial Intelligence: A Modern Approach" 英語版第三版 9.2 節 (p.328) より。
擬似コード
function unify(x, y, dic)
if dic == 失敗
return 失敗
else if x == y
return dic
else if x が変数
return unifyVar(x, y, dic)
else if y が変数
return unifyVar(y, x, dic)
else if x が 関数 かつ y が関数
return unify(xの引数, yの引数, unify(xの関数名, yの関数名, dic))
else if x がリスト かつ y がリスト
return unify(xの2番目以降, yの2番目以降, unify(xの先頭, yの先頭, dic))
else
return 失敗
function unifyVar(var, x, dic)
if var in dic
return unify(dic[var], x, dic)
else if x in dic
return unify(var, dic[x], dic)
else if var が x の中に含まれている
return 失敗
else
return dic に var = x を追加して dic を返す