尝试实现匹配，这是一种有限形式的统一。

如果我们能找到替换公式中变量的代换，使得两个公式在语法上等价，那么这两个公式就可以匹配。

我需要编写一个函数来判断一个与地面项对应的常量（例如Brother(George)）和一个与量化公式对应的模式（例如Brother(x)）是否匹配。如果它们匹配，函数将返回一个称为绑定的代换集，该集合将变量映射到项。一个常量与另一个常量匹配的前提是它们相等。一个未绑定的变量（当前没有绑定）可以匹配任何公式。一个已绑定的变量与一个常量匹配的前提是该常量与该变量所绑定的值相等。

示例：

match( Loves(Dog(Fred), Fred)

Loves(x,y))

为真，x = Dog(Fred) 且 y = Fred

另一个示例

match( Loves(Dog(Fred), Fred)

Loves(x,x)

失败

回答：

最一般统一器（MGUs）的概念在这里似乎很有用。解决方案方法如下所示。
让我们有一个初始的空集，命名为mgu，以及另一个空集E。

mgu = {}G = match(Loves(Dog(Fred),Fred),Loves(x,y))E = {Loves(Dog(Fred),Fred),Loves(x,y)}mgu = {Fred|y}             // 用y替换Fred，先替换变量。G = match(Loves(Dog(y),y),Loves(x,y))E = {Loves(Dog(y),y),Loves(x,y)}mgu = {Fred|y,Dog(y)|x}    // 用x替换Dog(y)G = match(Loves(x,y),Loves(x,y))  E = {Loves(x,y)}           // E在这里变成单例集，我们在这里停止。                           // 在此阶段无法进行更多替换。

match() 如果在无法进行更多替换时E变成单例集，则返回True，否则返回False。并且可以将mgu作为所需的代换集返回。

G = Truemgu = {Fred|y,Dog(y)|x}

另一个示例可以如下说明。

mgu = {}G = match(Loves(Dog(Fred),Fred),Loves(x,x))E = {Loves(Dog(Fred),Fred),Loves(x,x)}mgu = {Fred|x}             // 用x替换Fred。G = match(Loves(Dog(x),x),Loves(x,x))E = {Loves(Dog(x),x),Loves(x,x)}mgu = {Fred|x,Dog(x)|y}       // 用y替换Dog(x)G = match(Loves(y,x),Loves(x,x))  E = {Loves(y,x),Loves(x,x)}   // E在这里没有变成单例集。                              // 但在此阶段无法进行更多替换。

因此，

G = False