prolog - 我对这个特定程序的逻辑感到困惑

Question

问题:

Jack is looking at Anne, Anne is looking at George
Jack is married, George is not.

Is a married person looking at an unmarried person?

我正在查看在 this link 中找到的解决方案这需要:

unmarried(X) :- not(married(X)).
unmarried("George").
unmarried("Anne").

married("Jack").
married("Anne").

looking_at("Jack", "Anne").
looking_at("Anne", "George").

check(X, Y):-
    looking_at(X,Y),
    married(X),
    unmarried(Y).

完成这么多后，有几个问题会立即显现出来。对于第一部分，我很困惑为什么 Anne 被定义为 Married("Anne") 和 Unmarried("Anne")，但我很快就把它放在一边假设这可能意味着定义 Anne 已婚或未婚

A quick look at SO doesn't help either, as I found only some remotely related questions;
This particular question being the closest one.

现在回到我这里遇到的问题......

unmarried(X) :- not(married(X)). 处理操作，如果 Anne 作为 check(_, _)

that 的程序员解决方案已使用单个 check(_, _) 处理了它，据此:check(Anne,George) 将推断:

• 安妮看着乔治
• 安妮结婚了
• 乔治未婚

That compiler produces this result as:
Anne->Jack->Anne->Anne
George->Anne->George->George

此时，我不知道为什么编译器会产生这些结果。据我所知，this也没有给出解决方案。在我使用的旧桌面版 prolog 中，check(Anne,George). 应该会产生一个YES，因为所有条件都为真(嗯我从未尝试过在线 swi-prolog tbh；它有什么不同吗？)

对于 check(Jack,Anne) 是:

• jack 看着安妮
• jack 结婚了
• 安妮未婚

I don't see how this necessarily solves the problem. Could someone post a better solution or explain in detail how this is working?

---

要求:

我需要解决我在这个问题开头发布的问题。如果您可以根据我发布的现有条件解决它，那就太好了。但是，我也愿意接受其他想法和解决方案。

---

Answer 1

首先让我们看看拼图本身。问题是“已婚的人在看未婚的人吗？”显然是一个是/否问题。考虑到我们的婚姻状况，我们的知识不完整(安妮)。我们所知道的婚姻状况的人都没有互相凝视，所以我们不得不考虑安妮来寻找答案。如果我们假设:

• Anne 已婚，那么答案是肯定的，因为她正在看未婚的 George。

• 安妮没有结婚，那么答案是肯定的，因为已婚的 jack 正在看着她。

所以无论哪种方式，都有一个已婚的人在看着一个未婚的人，因此这个谜题的答案是肯定的。

关于给定的解决方案:我认为作者试图通过 married("Anne") 和 的事实来模拟“Anne 要么已婚要么 未婚” >unmarried("Anne"). 然而事实似乎表明，Anne 同时处于已婚和未婚状态。此外，规则 unmarried(X) :- not(married(X)). 结合事实 married/1 和 unmarried/1 两次产生解决方案“Anne”。因此 check/2 也两次产生 Anne-looks-at-George 解决方案:

    ?- check(X,Y).
X = "Jack",
Y = "Anne" ? ;
X = "Anne",
Y = "George" ? ;
X = "Anne",
Y = "George"

我可以看出作者试图用他的解决方案去哪里，但它并没有真正表达其中涉及的假设以及这两个独特的解决方案是如何联系起来的。

我的尝试如下:我会保留原始版本中的四个事实并为安妮添加另一个:

married(jack).

unmarried(george).

looking_at(jack,anne).
looking_at(anne,george).

unknown(anne).

然后我可以对我不知道的人的婚姻状况做出假设:

person_assumption(A,married) :- unknown(A).
person_assumption(A,unmarried) :- unknown(A).

现在回答是的相关案例是:(1) 一个已知的未婚者正在被一个已知的已婚者看，以及 (2) 一个人 P1 是

• 在假设 P1 已婚的情况下查看已知的未婚人士

和

• 在假设 P1 未婚的情况下被一个已知的已婚人士看

谓词 problematicgaze/1 正在对这些观察结果进行建模:

problematicgaze((P1-P2)) :-                                   % case (1)
    married(P1),
    unmarried(P2),
    looking_at(P1,P2).
problematicgaze((if_married(P1)-P2,P3-if_unmarried(P1))) :-   % case (2)
    assumedproblematic(if_married(P1),P2),
    assumedproblematic(P3,if_unmarried(P1)).


assumedproblematic(if_married(P1),P2) :-
    person_assumption(P1,married),
    unmarried(P2),
    looking_at(P1,P2).
assumedproblematic(P1,if_unmarried(P2)) :-
    person_assumption(P2,unmarried),
    married(P1),
    looking_at(P1,P2).

这可以分解为:要么我得到一个解决方案并且答案是是，要么谓词失败并且答案是否。所以我问在给定情况下是否存在有问题的凝视:

   ?- problematicgaze(G).
G = (if_married(anne)-george,jack-if_unmarried(anne)) ? ;
no

正如预期的那样，problematicgaze/1 的第一条规则没有答案，但第二条规则没有答案。无论对安妮采取哪种假设，已婚人士都在看未婚人士。除此之外，没有找到解决方案。