统一是通过查找替换使两个不同的逻辑原子表达式相同的过程。统一取决于替换过程。
它将两个文字作为输入,并使用替换使它们相同。
让Ψ 1 和Ψ 2 是两个原子句子,并且𝜎成为统一体,Ψ 1 𝜎 =Ψ 2 𝜎 ,则可以表示为 UNIFY(Ψ 1 ,Ψ 2 ) 。
示例: 查找Unify {King(x),King(John)}的MGU
使用UNIFY算法进行统一,该算法采用两个原子语句并返回这些语句的统一符(如果存在)。
统一是所有一阶推理算法的关键组成部分。
如果表达式彼此不匹配,则返回失败。
替换变量称为"最通用统一者"或MGU。
在第一个表达式中将x替换为a,将y替换为f(z),并将其表示为 a/x 和f(z)/y。
通过两个替换,第一个表达式将与第二个表达式相同,并且替换集将为: [a/x,f(z)/y] 。
谓词符号必须相同,具有不同谓词符号的原子或表达式永远不能统一。
两个表达式中的参数个数必须相同。
如果同一表达式中存在两个相似的变量,统一将失败。
Step. 1: If Ψ1 or Ψ2 is a variable or constant, then:
a) If Ψ1 or Ψ2 are identical, then return NIL.
b) Else if Ψ1is a variable,
a. then if Ψ1 occurs in Ψ2, then return FAILURE
b. Else return { (Ψ2/ Ψ1)}.
c) Else if Ψ2 is a variable,
a. If Ψ2 occurs in Ψ1 then return FAILURE,
b. Else return {( Ψ1/ Ψ2)}.
d) Else return FAILURE.
Step.2: If the initial Predicate symbol in Ψ1 and Ψ2 are not same, then return FAILURE.
Step. 3: IF Ψ1 and Ψ2 have a different number of arguments, then return FAILURE.
Step. 4: Set Substitution set(SUBST) to NIL.
Step. 5: For i=1 to the number of elements in Ψ1.
a) Call Unify function with the ith element of Ψ1 and ith element of Ψ2, and put the result into S.
b) If S = failure then returns Failure
c) If S ≠ NIL then do,
a. Apply S to the remainder of both L1 and L2.
b. SUBST= APPEND(S, SUBST).
Step.6: Return SUBST.
检查相同的表达式匹配项。
如果一个表达式是变量v i ,而另一个表达式是不包含变量v i 的项t i ,则: 将t i /v i 替换为现有替换 将t i /v i 添加到替换集列表中。 如果两个表达式都是函数,则函数名称必须相似,并且两个表达式中的参数数目必须相同。
统一者: {11/y}。