我了解反向链接算法的大部分内容(用于一阶逻辑(，但不了解Standardize-Variables(rule)的作用。下面是算法的伪代码：
function FOL-BC-Ask(KB, query) returns a generator of substitutions
return FOL-BC-Or(KB, query, {})
function FOL-BC-Or(KB, goal, θ) returns a substitution
for each rule in Fetch-Rules-For-Goal(KB, goal) do
(lhs ⇒ rhs) ← Standardize-Variables(rule)
for each θ' in FOL-BC-And(KB, lhs, Unify(rhs, goal, θ)) do
yield θ'
function FOL-BC-And(KB, goals, θ) returns a substitution
if θ = failure then return
else if Length(goals) = 0 then yield θ
else
first, rest ← First(goals), Rest(goals)
for each θ' in FOL-BC-Or(KB, Subst(θ, first), θ) do
for each θ'' in FOL-BC-And(KB, rest, θ') do
yield θ''
我正在学习《人工智能-现代方法》一书，代码就是从那里来的。这本书只是简单地说
FOL BC Or的工作原理是获取所有可能与目标统一的子句，将子句中的变量标准化为全新的变量，然后。。。
我确实理解这一点，但我不理解为什么需要这样做，或者如果没有它会发生什么。
我希望有人能解释一下。非常感谢。
将变量标准化的原因很普通：范围。一个变量是"；本地"；对于它的子句，所以当它出现在多个子句中时，它确实应该在每个子句中被视为不同的变量。分开标准化可以通过在每个子句中使用不同的名称来确保这一点。
让我更详细地解释一下。在规范化的一阶逻辑理论中，每个子句都隐含地普遍量化。如果我有两个条款的理论
快乐(X(
快乐(X(或不是朋友(X，Y(，
它的含义与相同
所有X：快乐(X(
对于所有X：对于所有Y：快乐(X(或不是朋友(X，Y(
你可以想到"；对于所有X〃；作为一种"；声明"；X(在"声明"的编程意义上(，所以可以说，这些变量中的每一个都是"；本地"；对于子句，在相同的意义上，编程中的局部变量是其作用域的局部变量。两个子句中都使用了X，这纯属巧合，事实上，我们可以在每个子句中随意重命名它们，并获得完全等价的理论，如
对于所有U：快乐(U(
对于所有V：对于所有W：快乐(V(或不是朋友(V，W(
甚至
所有X：快乐(X(
对于所有Y：对于所有X：快乐(Y(或不是朋友(Y，X(
分开标准化是有作用的，因为如果我们试图统一这两个子句，就会有两个变量具有相同的名称X，尽管它们不一定指代相同的实体。如果我们试图在不首先标准化的情况下统一上面的两个条款，我们将统一X和Y，最终得到
快乐(X(或不是朋友(X，X(
这意味着"；朋友"；是相同的，即使如果我们简单地重命名变量，就意味着而不是。使用U、V、W名称将相同的完全等价的两个子句统一在中
快乐(U(或不是朋友(U，W(
其中现在的两个论点"；朋友"；不需要相同。
事实上，我们从统一完全等价的理论中获得了不同的结果，这表明有些东西一定是不正确的。事实上，这里不正确的是将使用相同名称(X(的变量的两个子句统一起来，尽管它们实际上不是同一个变量，并且可以等效地重命名为其他变量。
David Einsentat的评论是正确的，即未能标准化分离是不正确的，因为它没有提供最通用的统一器，因为它可能提供了一个具有虚假约束的统一器(如我们上面看到的平等(，使其无法达到应有的通用性。
分开标准化通过将变量重命名为"0"来解决这个问题；全新的"；，这意味着变量不会出现在其他任何地方，因此不会带来以这种方式碰撞和引入基于纯粹任意名称选择的错误相等的风险。