人工智能匹配,统一

Matching in Artificial intelligence, unification

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

尝试匹配两个公式,如果我们能找到替代项 出现在公式中的变量使得两者在句法上是 相当于.

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

示例:

match( Loves(Dog(Fred), Fred)

Loves(x,y))

is true with x = Dog(Fred) and y = Fred

另一个

match( Loves(Dog(Fred), Fred)

Loves(x,x)

fails

MGU 的概念,即 大多数通用统一器 似乎在这里很有用。解决方法如下所示。
让我们有一个名为 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.

match() returns True if E 成为单例集当不可能有更多替换时,否则 Falsemgu 可以作为所需的替换集返回。

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