我有以下事实（el代表大象）：

el(Sam)    el(Clyde)    el(Oscar)pink(Sam)gray(Clyde)  likes(Clyde, Oscar)pink(Oscar)Vgray(Oscar)    likes(Oscar, Sam)

现在，我想证明：某个灰色大象喜欢某个粉色大象，这可以翻译为：（存在 x）（el(x) ∧ gray(x) ∧ （存在 y） (el(y) ∧ pink(y) ∧ likes(x, y))。因此，我们需要取其否定并将其解析到基础中，以便达到空集(？)。

否定是（将使用 ~ 表示否定）：

~el(x) V ~gray(x) V ~el(y) V ~pink(y) V ~likes(x, y)

依我看，我应该为 x 和 y 分配值（Sam, Clyde 或 Oscar）并将后面的语句插入基础中，以“消除”已经存在的事实。

我的尝试：

我设 x = Clyde, y = Oscar，这给了我：

~el(Clyde) V ~gray(Clyde) V ~el(Oscar) V ~pink(Oscar) V ~likes(Clyde, Oscar)

如果我将其放入基础中，会“消除”它们的“配对”，基础变为：

el(Sam)pink(Sam)gray(Oscar)    likes(Oscar, Sam)

现在怎么办？我们的大象用完了！

理想情况下，我希望设 x' = Oscar, y' = Sam，这样我会得到：

~el(Oscar) V ~gray(Oscar) V ~el(Sam) V ~pink(Sam) V ~likes(Oscar, Sam)

这将进入基础并消除一切，但 ~el(Oscar) 仍然存在！我应该如何继续？

后续问题：

基础：

abc V d

然后我将 ~a/\~b/\~c/\~d 放入基础中。基础中的一切都会以相同的方式消失吗？我是说，V 运算符不会影响事情吗？

回答：

你可以有这样的内容：

 el(sam). el(clyde). el(oscar). pink(sam). grey(clyde). likes(clyde,oscar). likes(oscar,sam). canbe(oscar,grey). canbe(oscar,pink). gelephant_likes_pelephant(GE,PE):-   grey(GE),el(GE),   pink(PE),el(PE),   likes(GE,PE). gelephant_likes_pelephant(GE,PE):-   canbe(GE,grey),el(GE),   pink(PE),el(PE),   likes(GE,PE).gelephant_likes_pelephant(GE,PE):-  grey(GE),el(GE),  canbe(PE,pink),el(PE),  likes(GE,PE).

问题：

?- gelephant_likes_pelephant(GE,PE).GE = oscar,PE = sam ;GE = clyde,PE = oscar.

你必须小心如何使用像 canbe/2 这样的谓词。因为它表示 oscar 可以是灰色或粉色。然后我的查询是在问哪些灰色大象喜欢哪些粉色大象，答案可以解释为：如果 oscar 是灰色大象，那么 oscar 喜欢 sam，或者如果 clyde 喜欢 oscar，那么 oscar 是粉色大象。