prolog中的命题逻辑几乎可以工作，xor有问题

Question

我对 prolog 很陌生，所以我正在尝试制作一个命题逻辑求解器，可以解决这个问题：

这个想法是在像这样咨询时传递 p,q,r,s 布尔参数（仅作为示例）：

solvelogic(true,true,false,true).

所以我有这个知识库：

implies(X,Y) :- (not(X);Y).                       %that's implies formula and it works
xor(X,Y) :- not(X=Y).                             %that's xor formula and it works too
and(X,Y) :- X,Y.
or(X,Y) :- X;Y.

implies1(P,Q,R) :- implies(and(P,Q),R).
implies2(P,Q,R) :- implies(P,(or(not(Q),R))).
implies3(P,Q,R) :- implies(implies1(P,Q,R),implies2(P,Q,R)).

所以我可以通过咨询来测试我的代码是否有效：

现在没关系，但让我们尝试使用最终的异或，它会接受我需要的整个命题：

它返回true，这是错误的，因为如果implies3(true,true,true)returns true，那么xor(implies3(true,true,true),true)应该返回false，但事实并非如此。

我可以证明 xor(X,Y) 有效：

没错，它返回 false，但我不知道当我咨询 xor(implies3(true,true,true),true) 时发生了什么，它应该返回“false”但它没有，即使它与异或（真，真）。

可能是什么问题？我想我已经很接近了！

Answer 1

所以，为了解决您的问题，您可以用这种方式重写您的 xor/2 谓词：

nand(A,B):- 
    not(and(A,B)).

xor(A,B):- 
    or(A,B), 
    nand(A,B). 

还有查询：

?- xor(implies3(true,true,true),true) 
false

xor/2的实现遵循这样的思路：or的真值表是0111，and的真值表是1000所以nand是0111。逗号, 像and 一样工作，所以0110 and 0111 是0110，这是xor 的真值表。

Answer 2

你可以试试

eval(P,R) :- P -> R=true ; R=false.

%xor(X,Y) :- not(X=Y).                  %that's xor formula and it works too
xor(X,Y) :- eval(X,A),eval(Y,B), A\=B.

请注意，我具体化了论点...并建议相应地修改您的代码