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没有出现在规则的头部，所以它的通用量词可以移动到规则体中作为存在q uantifier：

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

现在，这个公式读为：如果存在一个Y使得friend_of(X,Y)为真FORALLXfriend(X)是真实的。这似乎与你想要的非常接近。

如果您考虑事实另一方面，他们习惯于说明情况。在上面的例子中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