computer-science - 一阶逻辑中统一的真实世界示例？

Question

我知道这只是编程问题的一部分，但目前，我正在做一些逻辑编程。我仍然没有正确理解的一件事是一阶逻辑中的统一。

我读了 Wikipedia article并且或多或少很清楚，目的是搜索一个将两个句子统一起来的术语......本文中也有示例，但我只是不明白为什么这应该有用。任何人都可以举一个真实世界对象而不是 A、B、C 等的例子吗？我希望这会帮助我理解。谢谢

Answer 1

感谢您提供这些详细的答案。现在我真的明白了。但是，我想在这里写下我在 Stuart Russell 和 Peter Norvig 的“人工智能:一种现代方法”一书中找到的一个例子，以防有人再次寻找同样的问题。我认为这个答案使用了一种非常实用的方法:

Lifted inference rules require finding substitutions that make different logical expressions look identical. This process is called unification and is a key component of all first-order inference algorithms. The UNIFY algorithm takes two sentences and returns a unifier for them if one exists.

Let us look at some examples of how UNIFY should behave. Suppose we have a query Knows(John, x): whom does John know? Some answers to this query can be found by finding all sentences in the knowledge base that unify with Knows(John, x). Here are the results of unification with four different sentences that might be in the knowledge base:

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

The last unification fails because x cannot take on the values John and Elizabeth at the same time.