一阶逻辑统一的现实世界例子?

如果你在看使用统一并且有用的实际例子,那么看看计算语言学中使用的基于统一的语法,例如hpsg和lfg。从表面上看,这看起来像是另一种统一的味道,但它们确实是一样的。

基于统一的语法可以被认为是一种CFG(上下文无关语法),在这种语法中,生成的内容会随着统一而扩展。CGF中的每个术语都会得到一个AVM(属性值矩阵),它是一个特征和值的有向非循环图。这里的想法有点类似于编译器中使用的属性语法。

想象一下这个玩具语法:

 S -> NP VP  
 NP -> Kim  
 NP -> The cats  
 VP -> V NP  
 V -> see  
 V -> sees

在协议中,我们有一些轻微的过度生成:

*猫看见了金 [S[NP猫][副总裁[V看到][NP金]]

为了解决这一问题,我们可以改进CFG,使其包含协议的概念:

 S -> NP_sg VP_sg  
 S -> NP_sg VP_pl  
 NP_sg -> Kim  
 NP_pl -> The cats  
 VP_sg -> V_sg NP_sg  
 VP_sg -> V_sg NP_pl  
 V_sg -> sees  
 V_pl -> see  
 VP_pl -> V_pl NP_pl  
 VP_pl -> V_pl NP_sg

在这里,我们将拒绝过去的过度生成。但这很快就导致了组合移植。然而,当我们分析以下内容时,我们可以用AVM扩展每个术语,并将它们统一起来:

 S -> NP VP , C = A unified with B.  
 NP -> kim /[ AGR sg ]. We mark Kim as being singular   
 NP -> The cats / [ AGR pl ]  
 VP[ AGR #1 ] -> V [ AGR #1 ] NP 

_1符号是可重入符号,这意味着该特性的值必须相同,事实上,它们在统一后将指向图中的同一节点,如果成功。在实践中,我们认为动词短语的一致性特征与短语中动词的一致性相同。

 V -> See / [ AGR pl ]  
 V -> Sees / [ AGR sg ]

由于NP和VP无法统一,因此我们的增强玩具语法“Kim see the cats”被拒绝,因为它的AGR特性具有不同的值。 当我们分析时,我们将AVM统一在一起,因此获得了非常多的表达能力,使语法工程师很容易编写语法。通常,广泛覆盖的UBG有100条规则,而等量CFG,可能不存在,具有统一性的CFG图灵完备,将有数千条或更多的规则。

有关详细信息,请参阅 HPSG 和 LFG .

感谢您提供这些详细的答案。现在我真的明白了。不过,我想在这里写一个我在斯图尔特·罗素和彼得·诺维格的《人工智能:现代方法》一书中找到的例子,以防有人再次寻找同样的问题。我认为这个答案使用了一种非常实际的方法:

提升的推理规则需要找到 不同的替代品 逻辑表达式看起来完全相同。 这个过程被称为统一和 是所有一级产品的关键组成部分 推理算法。统一 算法需要两个句子和 返回它们的unifier如果一个 存在。

让我们看一些例子 统一应该表现出来。假设我们有一个 查询知道(约翰,X):约翰是谁 知道吗?这个问题的一些答案可以 通过查找 与之相结合的知识库 知道(约翰,X)。这是结果 四个不同的统一 可能在 知识库:

UNIFY(Knows(John, x), Knows(John, Jane)) = {x/Jane}
UNIFY(Knows(John, x), Knows(y, Bill)) = {x/Bill, y/John}
UNIFY(Knows(John, x), Knows(y, Mother(y))) = {y/John, x/Mother(John)}
UNIFY(Knows(John, x), Knows(x, Elisabeth)) = fail

最后一次统一失败是因为x 不能接受约翰和 同时伊丽莎白。

逻辑编程,阿法克,几乎是统一的。您向解释器提供一条语句,解释器试图将其与它知道是“真”的东西(即数据库中的东西)统一起来。

例如

cat(tom) :- true.

断言汤姆是只猫。

然后你可以查询

?- cat(X).

Prolog会回来

 X = tom

Prolog在其数据库中查找并尝试统一所提供的语句( cat(X) )事实上,它已经“知道”。在这种情况下,它发现 cat(tom) 因此可以告诉你 X=tom .