序言中的逻辑否定 [英] Logical Negation in Prolog
问题描述
我已经阅读了很多有关Prolog的否定失败的信息，其中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是arity 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 证明了失败否定"仅与基本从句兼容/相似于经典否定.我了解例如:
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
Law of excluded middle: p \/ ~p
这里是一个例子，请看这个逻辑程序 和这些查询:
Here is an example, take this logic program and these queries:
p :- p
?- \+(p, \+p)
?- p; \+p
逻辑程序的Clark完成是 如下，否定为失败查询 执行将产生以下内容:
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完成解决谓词定义的问题
和负面信息.另请参见
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.
这篇关于序言中的逻辑否定的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
