Prolog中的逻辑否定 [英] Logical Negation in Prolog

问题描述

我已经阅读了很多关于 Prolog 的 Negation by Failure 的内容，其中 Prolog 为了证明 +Goal 成立试图证明 Goal失败.

I've read quite a bit about Prolog's Negation by Failure where Prolog in order to prove that +Goal holds tries to prove that Goal fails.

这与 CWA(近距离世界假设)高度相关，例如，如果我们查询 +P(a)(其中 P是元数 1) 的谓词，我们没有任何线索可以证明 P(a) Prolog 假设(由于 CWA)not P(a) 成立，所以 +P(a) 成功.

This is highly connected with CWA (close world assumption) where for example if we query +P(a) (where P is a predicate of arity 1) and we have no clues that lead to prove P(a) Prolog assumes (due to CWA) that not P(a) holds so +P(a) succeeds.

根据我的搜索，这是一种解决经典逻辑弱点的方法，如果我们不知道 P(a) 那么我们无法回答是否 +P(a) 成立.

From what I've searched this is a way to solve classical logic weakness where if we had no clue about P(a) then we could not answer whether +P(a) holds.

上面描述的是在 Prolog 中引入非单调推理的方式.此外，有趣的部分是 Clark 证明了 Negation by Failure 与经典否定仅适用于基础条款兼容/相似.我理解例如:

What described above was the way of introducing non-monotonic reasoning in Prolog. Moreover the interesting part is that Clark proved that Negation by Failure is compatible/similar with classical negation only for ground clauses. I understand that for example:

X=1, +X==1.:应该在 Prolog(和经典逻辑)中返回 false.

X=1, +X==1.: should return false in Prolog (and in classical Logic).

+X==1, X=1.:在经典逻辑中应该返回 false，但在 Prolog 中成功，因为检查 NF 的时间 X 不是绑定，这与经典的纯逻辑不同.

+X==1, X=1.: should return false in classical logic but it succeeds in Prolog since the time that NF is examined X is not bound, this differs from classic-Pure Logic.

+X==1.:在 X 被绑定之前不应该在经典逻辑中给出任何答案，但在 Prolog 中它返回 false(可能是为了打破经典逻辑)，这与纯逻辑不同/不兼容.

+X==1.: should not give any answer in classical logic until X is bound, but in Prolog it returns false (possibly to break weakness of classical logic) and this is not same/compatible with pure Logic.

我的尝试是模拟经典的否定，感谢@false在评论中的建议，目前的实现是:

My attempt was to simulate classic negation, thanks to @false's suggestions in comments, current implementation is:

\+(Goal) :- when(ground(Goal), +Goal). 

一些测试:

?- \+(X==1).
when(ground(X), +X==1).

?- X=1, \+(X==1).
false.

?- \+(X==1), X=1.
false. 

我的问题:

以上是对经典否定的正确解释吗?(是否有任何明显的角落案例遗漏了??我还担心使用 when/2 时的逻辑纯度，可以安全地假设上述内容是纯的吗??).

Is the above a correct interpretation of classical negation? (Are there any obvious corner cases that it misses?? also I'm concerned about Logic Purity when using when/2, is it safe to assume that the above is pure??).

推荐答案

Prolog 不能做经典的否定.由于它不使用经典推理.即使在克拉克面前完成后，它无法检测到以下内容两条经典定律:

Prolog cannot do classical negation. Since it does not use classical inference. Even in the presence of Clark completion, it cannot detect the following two classical laws:

不矛盾定律:~(p/ ~p)

Law of noncontradiction: ~(p / ~p)

排中律:p /~p

这里是一个例子，取这个逻辑程序以及这些查询:

Here is an example, take this logic program and these queries:

   p :- p

   ?- +(p, +p)

   ?- p; +p

逻辑程序的克拉克完成是如下，否定为失败查询执行产生以下结果:

The Clark completion of the logic program is as follows and the negation as failure query execution yields the following:

   p <-> p

   loops

   loops

Clark 补全解决了谓词定义的问题和负面信息.另见 5.2 规则和部分他们的完成.另一方面，当没有谓词时有定义，CLP(X) 有时可以同时执行这两个定律，当一个否定运算符被定义为 deMorgan 风格时.这是CLP(B) 的否定运算符:

Clark completion adresses the issue of predicate definitions and negative information. See also section 5.2 Rules and their Completion. On the other hand, when no predicate definitions are around, CLP(X) can sometimes do both laws, when a negation operator is defined deMorgan style. Here is a negation operator for CLP(B):

?- listing(neg/1).
neg((A;B)) :-
    neg(A),
    neg(B).
neg((A, _)) :-
    neg(A).
neg((_, A)) :-
    neg(A).
neg(neg(A)) :-
    call(A).
neg(sat(A)) :-
    sat(~A).

这是一些执行:

?- sat(P); neg(sat(P)).
P = 0 
P = 1.
?- neg((sat(P), neg(sat(P)))).
P = 0 
P = 1.

当否定影响域时，CLP(X) 也会出现问题，通常是有限的，然后会变得无限.因此对于例如一个约束，如 (#=)/2, ... 不应该是一个问题，因为它可以被一个约束 (#=)/2, ... 替换.

CLP(X) will also have problems when the negation affects domains, that are usually finite and that would then get infinite. So for example a constraint such as (#=)/2, ... shouldn't be a problem, since it can be replaced by a constraint (#=)/2, ... .

但是当应用于约束时，对 CLP(FD) 的否定通常不起作用(中)/2.如果 CLP(X) 系统提供物化.在这种情况下，析取可以比仅使用 Prolog 回溯析取更智能一点.

But negation for CLP(FD) will usually not work when applied to constraints (in)/2. The situation can slightly be mitigated if the CLP(X) system offers reification. In this case the disjunction can be rendered a little bit more intelligent than just using Prolog backtracking disjunction.

这篇关于Prolog中的逻辑否定的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！