Prolog事实中的存在量化

Question

我正在Prolog(swi-prolog)中做我的第一步,无法解决以下问题:如何将存在量化的规则包括在我的事实中; 具体来说,我怎么能把句子"每个人都是某人的朋友" \forall x \exists y friend(x,y)作为一个事实呢？到目前为止我发现的每一个问题都只是关于查询而不是事实 谢谢!

Answer 1

在您给出的示例中,您实际上是在量化变量而不是规则.考虑到这一点,请考虑以下示例:

friend_of(a,b).

friend(X) :-
   friend_of(X,Y).

规则中的变量是普遍量化的,因此您可以将规则编写为逻辑公式,如下所示:

∀ X∀ Y (friend(X)←friend_of(X,Y))

由于变量Y不会出现在规则的头部,因此它的通用量词可以作为存在量词移动到规则体中:

∀ X (friend(X)←∃Y friend_of(X,Y))

现在,这个公式如下:FORALL X friend(X) 如果存在是真实的 Y ,从而 friend_of(X,Y) 是真实的.这似乎非常接近你想要的.

另一方面,如果你考虑事实,他们习惯于陈述某些情况.上例中的事实friend_of/2只是写作的简短方法

friend_of(a,b) :- true.

但是,这里没有变量,所以没有什么可以量化的.

编辑:关于你的评论中的情况,我会注意到谓词构成了关系.关系不是必然对称的,这就是我将关系命名为friend_of/2的原因.也就是说,friend_of(a,b)不一定意味着friend_of(b,a).关系也不是必然的反身.关系朋友是否反身是有争议的.但是,它肯定是一种可能的阅读.考虑到这一点以及评论中的给定示例,让我们假设您有一些描述的事实a,b并且c像人一样:

person(a).
person(b).
person(c).

然后你可以描述朋友/ 2的反身关系:

friends(a,b) :- false.   % example from your comment
friends(a,c) :- false.   % example from your comment
friends(X,X) :-          % the relation is reflexive
   person(X).            % among people

表达反身性的规则基本上表明,每个人至少都是他/她自己的朋友.从这个规则你的要求每个人都是直接跟随的人的朋友.如果您查询此关系,您将获得所需的结果:

   ?- friends(a,X).
X = a

尽管两个不同的人之间没有真正的友谊,但最常见的查询也会为每个人产生结果:

   ?- friends(X,Y).
X = Y = a ? ;
X = Y = b ? ;
X = Y = c

请注意,事实人/ 1是必要的,以限制对实际人的答案.如果你与一些非人查询朋友/ 2:

   ?- friends(cos(0),X).
no

如果你试图在没有这个目标的情况下定义反身性:

friend(X,X).

你的定义太笼统了:

   ?- friends(a,X).           % desired result
X = a
   ?- friends(cos(0),X).      % undesired result
X = cos(0)

最通用的查询不会产生任何实际的人:

   ?- friends(X,Y).
X = Y