prolog - 统一扩展项，双重否定

Question

我需要引入一个谓词来否定原子。到目前为止，我有neg(Premise) :- \+ Premise.，这给了我以下结果：

?- assert(a).
true.

?- a.
true.

?- neg(a).
false.

?- neg(neg(a)).
true.

这是有道理的，一切都是花花公子，直到我尝试统一。例如

[a,_] = [a,123].返回true.

尽管

[a,_] = [neg(neg(a)),123].返回false.。

我该如何解决这个问题，以便对neg(neg(X))零件进行评估或以其他方式统一X（因为它们在逻辑上都是等效的）？所以基本上，我需要X=neg(a), a=neg(X).成功。

编辑我找到了一个解释，为什么 not(not(<expression>))不等同<expression>于序言。既然<expression>成功了，not(<expression>)就失败了。当目标失败时，它实例化的变量将无法实例化。（来源，幻灯片 14）。

我仍然不确定如何解决这个问题。

Answer 1

真值的具体化将适用于您的简单案例：

4 ?- [user].
|: reify(P, V) :- call(P) -> V = 1 ; V = 0.
% user://1 compiled 0.03 sec, 2 clauses
true.

5 ?- reify(true, V), reify(\+ \+ true, U), V = U.
V = U, U = 1.

使用您的符号：

6 ?- [user].
|: a.
|: neg(P) :- \+ P.
% user://2 compiled 0.02 sec, 3 clauses
true.

7 ?- reify(a, V), reify(neg(neg(a)), U), V = U.
V = U, U = 1.

不确定这将如何与您的代码合并。