人工智能中的匹配、统一

Question

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

如果我们可以找到替换，则尝试匹配两个公式匹配 出现在公式中的变量使得两者在语法上 等价的。

我需要编写一个函数来确定是否 常数对应于一个基本项，例如 Brother(George) 和 模式对应于一个量化的公式，如 Brother(x) 匹配。如果 它们确实匹配函数返回一组称为绑定的替换 将变量映射到术语。一个常数匹配另一个常数，如果它们 是平等的。未绑定的变量（当前没有绑定的变量）匹配 任何公式。绑定变量匹配一个常量，如果该常量和 变量绑定的值相等。

例子：

match(爱(狗(Fred), Fred)

爱(x,y))

在 x = Dog(Fred) 和 y = Fred 时为真

另一个

match(爱(狗(Fred), Fred)

爱(x,x)

失败

Answer 1

MGU 的概念，即 Most General Unifiers 似乎在这里有用。解决方法如下图所示。
让我们有一个名为 mgu 的初始空集和另一个名为 E 的空集。

mgu = {}
G = match(Loves(Dog(Fred),Fred),Loves(x,y))
E = {Loves(Dog(Fred),Fred),Loves(x,y)}


mgu = {Fred|y}             // Replace Fred by y, variables to be replaced first.
G = match(Loves(Dog(y),y),Loves(x,y))
E = {Loves(Dog(y),y),Loves(x,y)}


mgu = {Fred|y,Dog(y)|x}    // Replace Dog(y) by x
G = match(Loves(x,y),Loves(x,y))  
E = {Loves(x,y)}           // E becomes a singleton set here, we stop here.
                           // No more substitutions are possible at this stage.

ma​​tch() 返回 True 如果 E 成为单例集且不能再进行替换，否则返回 False >。 mgu 可以作为所需的替换集合返回。

G = True
mgu = {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}             // Replace Fred by x.
G = match(Loves(Dog(x),x),Loves(x,x))
E = {Loves(Dog(x),x),Loves(x,x)}


mgu = {Fred|x,Dog(x)|y}       // Replace Dog(x) by y
G = match(Loves(y,x),Loves(x,x))  
E = {Loves(y,x),Loves(x,x)}   // E does not becomes a singleton set here.
                              // But no more substitutions are 
                              // possible at this stage.

因此，

G = False